introduces:  nonmap-range . 
 nonmap-range = ž .
open .

introduces: map , range , map of _ to _ , empty-map , disjoint-union _ , mapped-set _ . 

needs:      Tuples/Basics . map <= component .

 map 		= disjoint-union (map of element to range)* .
 range 		= nonmap-range | map  (disjoint) .
 map of _ to _ 	:: element, range -> map (total, injective) . 
 empty-map 		: map .
 disjoint-union _ 	:: map* -> map (partial, associative, commutative, unit is empty-map) .
 mapped-set _ 	:: map -> set (total) .
(1) disjoint-union ( ) = empty-map ;
	disjoint-union (map of e:element to r:range) = map of e:element to r:range .
     	intersection (mapped-set m1, mapped-set m2) is empty-set = true 
			=> disjoint-union (m1:map, m2:map) : map .
	intersection (mapped-set m1, mapped-set m2) is empty-set = false 
			=> disjoint-union (m1:map, m2:map) = nothing .
(2) mapped-set empty-map = empty-set ;
     	mapped-set map of e:element to r:range = set of e ;
     	mapped-set disjoint-union (m1:map, m2:map) 
			= disjoint-union (mapped-set m1, mapped-set m2) . 
 
closed except Generics .

introduces:  _ [ _to_ ] , _at_ , overlay_ , _restricted to_ , _omitting_ . 

includes:    Instant/Distinction ( map for s , _ is _ ) .

needs:       Tuples/Basics .

 _ [ _to_ ] 	:: map, element, range -> map . 
 _at_ 		:: map, element -> range (partial) . 
 overlay _ 	::  map* -> map  (total, associative, idempotent, unit is empty-map) . 
 _restricted to_ ::  map, set -> map (total) . 
 _omitting_ 	:: map, set -> map (total) . 
(1) (m <= map) [e <= element to r <= range] = m & disjoint-union (map of e to r)* .
(2) empty-map at e:element = nothing ;
	map of e':element to r:range at e:element 
		=  when e is e' then r 
      	disjoint-union (m:map, m':map) at e:element 
	    	= when there is disjoint-union (m, m') 
		    	then ((m at e)|(m' at e)) .
(3) overlay (m:map, m':map) = disjoint-union (m, m' omitting mapped-set m) .
(4) empty-map restricted to s:set = empty-map ;
     	map of e:element to r:range restricted to s:set 
	    	= if e is in s then map of e to r else empty-map ; 
      	disjoint-union (m:map, m':map) restricted to s:set 
	    	= when there is disjoint-union (m, m') 
		    	then disjoint-union (m restricted to s, m' restricted to s) .
(5) empty-map omitting s:set = empty-map ;
      	map of e:element to r:range omitting s:set =  
	    	if e is in s then empty-map else  map of e to r ; 
      	disjoint-union (m:map, m':map) omitting s:set 
	    	= when there is disjoint-union (m, m') 
		    	then disjoint-union (m omitting s, m' omitting s) .
(6) empty-map is m:disjoint-union (map of element to range)+ = false ;
      	map of e1:element to r1:range is  map of e2:element to r2:range 
	    	= if e1 is e2 then r1 is r2 else false ;
      	disjoint-union (map of e:element to r:range, m:map) is m':map 
	    	= when not (e is in mapped-set m) then if not (e is in mapped set m') 
		    	then false else both ((r is (m' at e)), (m is (m' omitting set of e)))  .