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

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

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

hence ex b_{1} being BinOp of (UAEnd UA) st

for x, y being Element of UAEnd UA holds b_{1} . (x,y) = y * x
; :: thesis: verum

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

proof

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

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

reconsider m = yy * xx as Element of UAEnd UA by Th3;

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 UAEnd UA by Th3;

take m ; :: thesis: S

thus S

for x, y being Element of UAEnd UA holds S

hence ex b

for x, y being Element of UAEnd UA holds b