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

proof

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;

hence X = Y by A5; :: thesis: verum