defpred S_{1}[ 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_{1}[x,y,z]
;

ex f being BinOp of the carrier of F st

for x, y being Element of F holds S_{1}[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

A1: for x, y being Element of F ex z being Element of F st S

ex f being BinOp of the carrier of F st

for x, y being Element of F holds S

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