defpred S_{1}[ 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_{1}[A1,A2,B]

for a, b being Element of Subspaces V holds S_{1}[a,b,o . (a,b)]
from BINOP_1:sch 3(A1);

hence ex b_{1} 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_{1} . (A1,A2) = W1 + W2
; :: thesis: verum

$3 = W1 + W2;

A1: for A1, A2 being Element of Subspaces V ex B being Element of Subspaces V st S

proof

ex o being BinOp of (Subspaces V) st
let A1, A2 be Element of Subspaces V; :: thesis: ex B being Element of Subspaces V st S_{1}[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_{1}[A1,A2,C]

thus S_{1}[A1,A2,C]
; :: thesis: verum

end;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

thus S

for a, b being Element of Subspaces V holds S

hence ex b

for A1, A2 being Element of Subspaces V

for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds

b