let R1, R2 be Relation of the carrier of (RLMSpace n); ( ( 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 ) )
; R1 = R2
now 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 ;
( ( [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 )
( [a,b] in R2 implies [a,b] in R1 )assume A5:
[a,b] in R2
;
[a,b] in R1then 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;
verum end;
hence
R1 = R2
by RELAT_1:def 2; verum