defpred S₁[ 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₁[x,y,m]

proof

let x, y be Element of UAEnd UA; :: thesis: ex m being Element of UAEnd UA st S₁[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₁[x,y,m]
thus S₁[x,y,m] ; :: thesis: verum

end;

ex B being BinOp of (UAEnd UA) st
for x, y being Element of UAEnd UA holds S₁[x,y,B . (x,y)] from BINOP_1:sch 3(A1);
hence ex b₁ being BinOp of (UAEnd UA) st
for x, y being Element of UAEnd UA holds b₁ . (x,y) = y * x ; :: thesis: verum