let h1, h2 be Function of (MapsT X),(TOL X); :: thesis: ( ( for m being Element of MapsT X holds h1 . m = cod m ) & ( for m being Element of MapsT X holds h2 . m = cod m ) implies h1 = h2 )
assume that
A3: for m being Element of MapsT X holds h1 . m = cod m and
A4: for m being Element of MapsT X holds h2 . m = cod 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 = cod m by A3
.= h2 . m by A4 ; :: thesis: verum

end;

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