defpred S₁[ set , set ] means ( [$1,$2] in R & ( for f being operation of A
for p, q being FinSequence st (p ^ <*$1*>) ^ q in dom f & (p ^ <*$2*>) ^ q in dom f holds
[(f . ((p ^ <*$1*>) ^ q)),(f . ((p ^ <*$2*>) ^ q))] in R ) );
thus ex D being Relation of the carrier of A st
for x, y being Element of A holds
( [x,y] in D iff S₁[x,y] ) from RELSET_1:sch 2(); :: thesis: verum