let h1, h2 be PartFunc of [:(MapsC X),(MapsC X):],(MapsC X); :: thesis: ( ( for l2, l1 being Element of MapsC X holds
( [l2,l1] in dom h1 iff dom l2 = cod l1 ) ) & ( for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds
h1 . [l2,l1] = l2 * l1 ) & ( for l2, l1 being Element of MapsC X holds
( [l2,l1] in dom h2 iff dom l2 = cod l1 ) ) & ( for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds
h2 . [l2,l1] = l2 * l1 ) implies h1 = h2 )
assume that
A12: for l2, l1 being Element of MapsC X holds
( [l2,l1] in dom h1 iff dom l2 = cod l1 ) and
A13: for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds
h1 . [l2,l1] = l2 * l1 and
A14: for l2, l1 being Element of MapsC X holds
( [l2,l1] in dom h2 iff dom l2 = cod l1 ) and
A15: for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds
h2 . [l2,l1] = l2 * l1 ; :: thesis: h1 = h2
A16: dom h1 = dom h2

proof

let x, y be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [x,y] in dom h1 or [x,y] in dom h2 ) & ( not [x,y] in dom h2 or [x,y] in dom h1 ) )
thus ( [x,y] in dom h1 implies [x,y] in dom h2 ) :: thesis: ( not [x,y] in dom h2 or [x,y] in dom h1 )

proof

assume A17: [x,y] in dom h1 ; :: thesis: [x,y] in dom h2
then reconsider l2 = x, l1 = y as Element of MapsC X by ZFMISC_1:87;
dom l2 = cod l1 by A12, A17;
hence [x,y] in dom h2 by A14; :: thesis: verum

end;

assume A18: [x,y] in dom h2 ; :: thesis: [x,y] in dom h1
then reconsider l2 = x, l1 = y as Element of MapsC X by ZFMISC_1:87;
dom l2 = cod l1 by A14, A18;
hence [x,y] in dom h1 by A12; :: thesis: verum

end;

now :: thesis: for l being Element of [:(MapsC X),(MapsC X):] st l in dom h1 holds
h1 . l = h2 . l

let l be Element of [:(MapsC X),(MapsC X):]; :: thesis: ( l in dom h1 implies h1 . l = h2 . l )
assume A19: l in dom h1 ; :: thesis: h1 . l = h2 . l
consider l2, l1 being Element of MapsC X such that
A20: l = [l2,l1] by DOMAIN_1:1;
A21: dom l2 = cod l1 by A12, A19, A20;
then h1 . [l2,l1] = l2 * l1 by A13;
hence h1 . l = h2 . l by A15, A20, A21; :: thesis: verum

end;

hence h1 = h2 by A16, PARTFUN1:5; :: thesis: verum