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

now :: thesis: for l being Element of MapsC X holds h1 . l = h2 . l

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

end;

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