defpred S₁[ set , set ] means for f being operation of A
for p, q being FinSequence holds
( (p ^ <*$1*>) ^ q in dom f iff (p ^ <*$2*>) ^ q in dom f );
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