defpred S_{1}[ 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_{1}[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

( 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

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