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

A12: for m2, m1 being Element of Maps V holds

( [m2,m1] in dom h1 iff dom m2 = cod m1 ) and

A13: for m2, m1 being Element of Maps V st dom m2 = cod m1 holds

h1 . [m2,m1] = m2 * m1 and

A14: for m2, m1 being Element of Maps V holds

( [m2,m1] in dom h2 iff dom m2 = cod m1 ) and

A15: for m2, m1 being Element of Maps V st dom m2 = cod m1 holds

h2 . [m2,m1] = m2 * m1 ; :: thesis: h1 = h2

A16: dom h2 c= [:(Maps V),(Maps V):] by RELAT_1:def 18;

A17: dom h1 c= [:(Maps V),(Maps V):] by RELAT_1:def 18;

A18: dom h1 = dom h2

( [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

A12: for m2, m1 being Element of Maps V holds

( [m2,m1] in dom h1 iff dom m2 = cod m1 ) and

A13: for m2, m1 being Element of Maps V st dom m2 = cod m1 holds

h1 . [m2,m1] = m2 * m1 and

A14: for m2, m1 being Element of Maps V holds

( [m2,m1] in dom h2 iff dom m2 = cod m1 ) and

A15: for m2, m1 being Element of Maps V st dom m2 = cod m1 holds

h2 . [m2,m1] = m2 * m1 ; :: thesis: h1 = h2

A16: dom h2 c= [:(Maps V),(Maps V):] by RELAT_1:def 18;

A17: dom h1 c= [:(Maps V),(Maps V):] by RELAT_1:def 18;

A18: 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 )

then reconsider m2 = x, m1 = y as Element of Maps V by A16, ZFMISC_1:87;

dom m2 = cod m1 by A14, A20;

hence [x,y] in dom h1 by A12; :: thesis: verum

end;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 A20:
[x,y] in dom h2
; :: thesis: [x,y] in dom h1
assume A19:
[x,y] in dom h1
; :: thesis: [x,y] in dom h2

then reconsider m2 = x, m1 = y as Element of Maps V by A17, ZFMISC_1:87;

dom m2 = cod m1 by A12, A19;

hence [x,y] in dom h2 by A14; :: thesis: verum

end;then reconsider m2 = x, m1 = y as Element of Maps V by A17, ZFMISC_1:87;

dom m2 = cod m1 by A12, A19;

hence [x,y] in dom h2 by A14; :: thesis: verum

then reconsider m2 = x, m1 = y as Element of Maps V by A16, ZFMISC_1:87;

dom m2 = cod m1 by A14, A20;

hence [x,y] in dom h1 by A12; :: thesis: verum

now :: thesis: for m being Element of [:(Maps V),(Maps V):] st m in dom h1 holds

h1 . m = h2 . m

hence
h1 = h2
by A18, PARTFUN1:5; :: thesis: verumh1 . m = h2 . m

let m be Element of [:(Maps V),(Maps V):]; :: thesis: ( m in dom h1 implies h1 . m = h2 . m )

consider m2, m1 being Element of Maps V such that

A21: m = [m2,m1] by DOMAIN_1:1;

assume m in dom h1 ; :: thesis: h1 . m = h2 . m

then A22: dom m2 = cod m1 by A12, A21;

then h1 . [m2,m1] = m2 * m1 by A13;

hence h1 . m = h2 . m by A15, A21, A22; :: thesis: verum

end;consider m2, m1 being Element of Maps V such that

A21: m = [m2,m1] by DOMAIN_1:1;

assume m in dom h1 ; :: thesis: h1 . m = h2 . m

then A22: dom m2 = cod m1 by A12, A21;

then h1 . [m2,m1] = m2 * m1 by A13;

hence h1 . m = h2 . m by A15, A21, A22; :: thesis: verum