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

end;

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