defpred S1[ Element of MSAEnd U1, Element of MSAEnd U1, set ] means $3 = $2 ** $1;
A1: for x, y being Element of MSAEnd U1 ex m being Element of MSAEnd U1 st S1[x,y,m]
proof
let x, y be Element of MSAEnd U1; :: thesis: ex m being Element of MSAEnd U1 st S1[x,y,m]
reconsider xx = x, yy = y as ManySortedFunction of U1,U1 ;
reconsider m = yy ** xx as Element of MSAEnd U1 by Th8;
take m ; :: thesis: S1[x,y,m]
thus S1[x,y,m] ; :: thesis: verum
end;
ex B being BinOp of (MSAEnd U1) st
for x, y being Element of MSAEnd U1 holds S1[x,y,B . (x,y)] from BINOP_1:sch 3(A1);
 hence ex b1 being BinOp of (MSAEnd U1) st
for x, y being Element of MSAEnd U1 holds b1 . (x,y) = y ** x ; :: thesis: verum