let X, Y be Function; :: thesis: ( dom X = dom A & ( for j being set st j in dom A holds

ex R being 1-sorted st

( R = A . j & X . j = the carrier of R ) ) & dom Y = dom A & ( for j being set st j in dom A holds

ex R being 1-sorted st

( R = A . j & Y . j = the carrier of R ) ) implies X = Y )

assume A5: ( dom X = dom A & ( for j being set st j in dom A holds

ex R being 1-sorted st

( R = A . j & X . j = the carrier of R ) ) & dom Y = dom A & ( for j being set st j in dom A holds

ex R being 1-sorted st

( R = A . j & Y . j = the carrier of R ) ) ) ; :: thesis: X = Y

for i being object st i in dom A holds

X . i = Y . i

ex R being 1-sorted st

( R = A . j & X . j = the carrier of R ) ) & dom Y = dom A & ( for j being set st j in dom A holds

ex R being 1-sorted st

( R = A . j & Y . j = the carrier of R ) ) implies X = Y )

assume A5: ( dom X = dom A & ( for j being set st j in dom A holds

ex R being 1-sorted st

( R = A . j & X . j = the carrier of R ) ) & dom Y = dom A & ( for j being set st j in dom A holds

ex R being 1-sorted st

( R = A . j & Y . j = the carrier of R ) ) ) ; :: thesis: X = Y

for i being object st i in dom A holds

X . i = Y . i

proof

hence
X = Y
by A5; :: thesis: verum
let i be object ; :: thesis: ( i in dom A implies X . i = Y . i )

assume i in dom A ; :: thesis: X . i = Y . i

then ( ex R being 1-sorted st

( R = A . i & X . i = the carrier of R ) & ex R being 1-sorted st

( R = A . i & Y . i = the carrier of R ) ) by A5;

hence X . i = Y . i ; :: thesis: verum

end;assume i in dom A ; :: thesis: X . i = Y . i

then ( ex R being 1-sorted st

( R = A . i & X . i = the carrier of R ) & ex R being 1-sorted st

( R = A . i & Y . i = the carrier of R ) ) by A5;

hence X . i = Y . i ; :: thesis: verum