defpred S1[ Element of Submodules V, Element of Submodules V, Element of Submodules V] means for W1, W2 being Submodule of V st $1 = W1 & $2 = W2 holds
$3 = W1 + W2;
A1: for A1, A2 being Element of Submodules V ex B being Element of Submodules V st S1[A1,A2,B]
proof
let A1, A2 be Element of Submodules V; :: thesis: ex B being Element of Submodules V st S1[A1,A2,B]
consider W1 being strict Submodule of V such that
A2: W1 = A1 by Def3;
consider W2 being strict Submodule of V such that
A3: W2 = A2 by Def3;
reconsider C = W1 + W2 as Element of Submodules V by Def3;
take C ; :: thesis: S1[A1,A2,C]
thus S1[A1,A2,C] by A2, A3; :: thesis: verum
end;
ex o being BinOp of (Submodules V) st
for a, b being Element of Submodules V holds S1[a,b,o . (a,b)] from BINOP_1:sch 3(A1);
 hence ex b1 being BinOp of (Submodules V) st
for A1, A2 being Element of Submodules V
for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds
b1 . (A1,A2) = W1 + W2 ; :: thesis: verum