let h1, h2 be Function of (MapsT X),(TOL X); :: thesis: ( ( for m being Element of MapsT X holds h1 . m = dom m ) & ( for m being Element of MapsT X holds h2 . m = dom m ) implies h1 = h2 )
assume that
A1: for m being Element of MapsT X holds h1 . m = dom m and
A2: for m being Element of MapsT X holds h2 . m = dom m ; :: thesis: h1 = h2

now :: thesis: for m being Element of MapsT X holds h1 . m = h2 . m

let m be Element of MapsT X; :: thesis: h1 . m = h2 . m
thus h1 . m = dom m by A1
.= h2 . m by A2 ; :: thesis: verum

end;

hence h1 = h2 by FUNCT_2:63; :: thesis: verum