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 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