let h1, h2 be PartFunc of [:(Maps V),(Maps V):],(Maps V); :: thesis: ( ( for m2, m1 being Element of Maps V holds
( [m2,m1] in dom h1 iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of Maps V st dom m2 = cod m1 holds
h1 . [m2,m1] = m2 * m1 ) & ( for m2, m1 being Element of Maps V holds
( [m2,m1] in dom h2 iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of Maps V st dom m2 = cod m1 holds
h2 . [m2,m1] = m2 * m1 ) implies h1 = h2 )
assume that
A10: for m2, m1 being Element of Maps V holds
( [m2,m1] in dom h1 iff dom m2 = cod m1 ) and
A11: for m2, m1 being Element of Maps V st dom m2 = cod m1 holds
h1 . [m2,m1] = m2 * m1 and
A12: for m2, m1 being Element of Maps V holds
( [m2,m1] in dom h2 iff dom m2 = cod m1 ) and
A13: for m2, m1 being Element of Maps V st dom m2 = cod m1 holds
h2 . [m2,m1] = m2 * m1 ; :: thesis: h1 = h2
A14: dom h1 c= [:(Maps V),(Maps V):] by RELAT_1:def 18;
A15: dom h2 c= [:(Maps V),(Maps V):] by RELAT_1:def 18;
A16: dom h1 = dom h2

proof

let x, y be set ; :: 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 m2 = x, m1 = y as Element of Maps V by A14, ZFMISC_1:106;
dom m2 = cod m1 by A10, A17;
hence [x,y] in dom h2 by A12; :: thesis: verum

end;

assume A18: [x,y] in dom h2 ; :: thesis: [x,y] in dom h1
then reconsider m2 = x, m1 = y as Element of Maps V by A15, ZFMISC_1:106;
dom m2 = cod m1 by A12, A18;
hence [x,y] in dom h1 by A10; :: thesis: verum

end;

now

let m be Element of [:(Maps V),(Maps V):]; :: thesis: ( m in dom h1 implies h1 . m = h2 . m )
assume A19: m in dom h1 ; :: thesis: h1 . m = h2 . m
consider m2, m1 being Element of Maps V such that
A20: m = [m2,m1] by DOMAIN_1:9;
dom m2 = cod m1 by A10, A19, A20;
then ( h1 . [m2,m1] = m2 * m1 & h2 . [m2,m1] = m2 * m1 ) by A11, A13;
hence h1 . m = h2 . m by A20; :: thesis: verum

end;

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