defpred S₁[ Element of F, Element of F, set ] means $3 = the addF of F . $1,((comp F) . $2);
A1: for x, y being Element of F ex z being Element of F st S₁[x,y,z] ;
ex f being BinOp of the carrier of F st
for x, y being Element of F holds S₁[x,y,f . x,y] from BINOP_1:sch 3(A1);
then consider S being BinOp of the carrier of F such that
A2: for x, y being Element of F holds S . x,y = the addF of F . x,((comp F) . y) ;
take S ; :: thesis: for x, y being Element of F holds S . x,y = the addF of F . x,((comp F) . y)
thus for x, y being Element of F holds S . x,y = the addF of F . x,((comp F) . y) by A2; :: thesis: verum