defpred S₁[ Element of Cosets N, Element of Cosets N, set ] means for A1, A2 being Subset of G st $1 = A1 & $2 = A2 holds
$3 = A1 * A2;
A1: for W1, W2 being Element of Cosets N ex V being Element of Cosets N st S₁[W1,W2,V]

proof

let W1, W2 be Element of Cosets N; :: thesis: ex V being Element of Cosets N st S₁[W1,W2,V]
reconsider A1 = W1, A2 = W2 as Subset of G by Th15;
reconsider C = A1 * A2 as Element of Cosets N by Th16;
take C ; :: thesis: S₁[W1,W2,C]
thus S₁[W1,W2,C] ; :: thesis: verum

end;

thus ex B being BinOp of (Cosets N) st
for W1, W2 being Element of Cosets N holds S₁[W1,W2,B . (W1,W2)] from BINOP_1:sch 3(A1); :: thesis: verum