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

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

hence
R1 = R2
by RELAT_1:def 2; :: thesis: verum( ( [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 )

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;thus ( [a,b] in R1 implies [a,b] in R2 ) :: thesis: ( [a,b] in R2 implies [a,b] in R1 )

proof

assume A5:
[a,b] in R2
; :: thesis: [a,b] in R1
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;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

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