defpred S1[ object , object ] means ex f being Function st
( f in the carrier of G & f . $1 = $2 );
consider R being Relation of the carrier of (RLMSpace n), the carrier of (RLMSpace n) such that
A1:
for x, y being object holds
( [x,y] in R iff ( x in the carrier of (RLMSpace n) & y in the carrier of (RLMSpace n) & S1[x,y] ) )
from RELSET_1:sch 1();
take
R
; for A, B being Element of (RLMSpace n) holds
( [A,B] in R iff ex f being Function st
( f in the carrier of G & f . A = B ) )
let A, B be Element of (RLMSpace n); ( [A,B] in R iff ex f being Function st
( f in the carrier of G & f . A = B ) )
thus
( [A,B] in R iff ex f being Function st
( f in the carrier of G & f . A = B ) )
by A1; verum