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

proof

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

end;

ex o being BinOp of (Subspaces V) st
for a, b being Element of Subspaces V holds S₁[a,b,o . (a,b)] from BINOP_1:sch 3(A1);
hence ex b₁ being BinOp of (Subspaces V) st
for A1, A2 being Element of Subspaces V
for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds
b₁ . (A1,A2) = W1 + W2 ; :: thesis: verum