defpred S₁[ 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) & S₁[x,y] ) ) from RELSET_1:sch 1();
take R ; :: thesis: 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); :: thesis: ( [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; :: thesis: verum