defpred S_{1}[ Element of MSAAut U1, Element of MSAAut U1, set ] means $3 = $2 ** $1;

A1: for x, y being Element of MSAAut U1 ex m being Element of MSAAut U1 st S_{1}[x,y,m]

for x, y being Element of MSAAut U1 holds S_{1}[x,y,IT . (x,y)]
from BINOP_1:sch 3(A1); :: thesis: verum

A1: for x, y being Element of MSAAut U1 ex m being Element of MSAAut U1 st S

proof

thus
ex IT being BinOp of (MSAAut U1) st
let x, y be Element of MSAAut U1; :: thesis: ex m being Element of MSAAut U1 st S_{1}[x,y,m]

reconsider xx = x, yy = y as ManySortedFunction of U1,U1 ;

reconsider m = yy ** xx as Element of MSAAut U1 by Th26;

take m ; :: thesis: S_{1}[x,y,m]

thus S_{1}[x,y,m]
; :: thesis: verum

end;reconsider xx = x, yy = y as ManySortedFunction of U1,U1 ;

reconsider m = yy ** xx as Element of MSAAut U1 by Th26;

take m ; :: thesis: S

thus S

for x, y being Element of MSAAut U1 holds S