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 for D1, D2 being Relation of the carrier of A st ( for x, y being Element of A holds
( [x,y] in D1 iff S₁[x,y] ) ) & ( for x, y being Element of A holds
( [x,y] in D2 iff S₁[x,y] ) ) holds
D1 = D2 from PUA2MSS1:sch 2(); :: thesis: verum