let R1, R2 be Relation of the carrier of (); :: thesis: ( ( for A, B being Element of () holds
( [A,B] in R1 iff ex f being Function st
( f in the carrier of G & f . A = B ) ) ) & ( for A, B being Element of () holds
( [A,B] in R2 iff ex f being Function st
( f in the carrier of G & f . A = B ) ) ) implies R1 = R2 )

assume that
A2: for A, B being Element of () holds
( [A,B] in R1 iff ex f being Function st
( f in the carrier of G & f . A = B ) ) and
A3: for A, B being Element of () holds
( [A,B] in R2 iff ex f being Function st
( f in the carrier of G & f . A = B ) ) ; :: thesis: R1 = R2
now :: thesis: for a, b being object holds
( ( [a,b] in R1 implies [a,b] in R2 ) & ( [a,b] in R2 implies [a,b] in R1 ) )
let a, b be object ; :: thesis: ( ( [a,b] in R1 implies [a,b] in R2 ) & ( [a,b] in R2 implies [a,b] in R1 ) )
thus ( [a,b] in R1 implies [a,b] in R2 ) :: thesis: ( [a,b] in R2 implies [a,b] in R1 )
proof
assume A4: [a,b] in R1 ; :: thesis: [a,b] in R2
then reconsider a1 = a, b1 = b as Element of () by ZFMISC_1:87;
ex f being Function st
( f in the carrier of G & f . a1 = b1 ) by A2, A4;
hence [a,b] in R2 by A3; :: thesis: verum
end;
assume A5: [a,b] in R2 ; :: thesis: [a,b] in R1
then reconsider a1 = a, b1 = b as Element of () by ZFMISC_1:87;
ex f being Function st
( f in the carrier of G & f . a1 = b1 ) by A3, A5;
hence [a,b] in R1 by A2; :: thesis: verum
end;
hence R1 = R2 by RELAT_1:def 2; :: thesis: verum