let R1, R2 be Relation of the carrier of (RLMSpace n); :: thesis: ( ( for A, B being Element of (RLMSpace n) 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 (RLMSpace n) 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 (RLMSpace n) 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 (RLMSpace n) 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 (RLMSpace n) 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 (RLMSpace n) 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