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