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

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

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

A1: for x, y being Element of Aut G ex m being Element of Aut G st S

proof

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

reconsider xx = x, yy = y as Homomorphism of G,G by Def1;

reconsider m = xx * yy as Element of Aut G by Th7;

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

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

end;reconsider xx = x, yy = y as Homomorphism of G,G by Def1;

reconsider m = xx * yy as Element of Aut G by Th7;

take m ; :: thesis: S

thus S

for x, y being Element of Aut G holds S