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

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

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

A1: for x, y being Element of UAAut UA ex m being Element of UAAut UA st S

proof

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

reconsider xx = x, yy = y as Function of UA,UA ;

reconsider m = yy * xx as Element of UAAut UA by Th6;

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

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

end;reconsider xx = x, yy = y as Function of UA,UA ;

reconsider m = yy * xx as Element of UAAut UA by Th6;

take m ; :: thesis: S

thus S

for x, y being Element of UAAut UA holds S