defpred S₁[ set , set , set ] means for W1, W2 being Subspace of M st $1 = W1 & $2 = W2 holds
$3 = W1 + W2;
A1: for A1, A2 being Element of Subspaces M ex B being Element of Subspaces M st S₁[A1,A2,B]

proof

let A1, A2 be Element of Subspaces M; :: thesis: ex B being Element of Subspaces M st S₁[A1,A2,B]
consider W1 being strict Subspace of M such that
A2: W1 = A1 by Def3;
consider W2 being strict Subspace of M such that
A3: W2 = A2 by Def3;
reconsider C = W1 + W2 as Element of Subspaces M by Def3;
take C ; :: thesis: S₁[A1,A2,C]
thus S₁[A1,A2,C] by A2, A3; :: thesis: verum

end;

thus ex o being BinOp of (Subspaces M) st
for A1, A2 being Element of Subspaces M holds S₁[A1,A2,o . (A1,A2)] from BINOP_1:sch 3(A1); :: thesis: verum