let V be RealLinearSpace; for W1, W2 being Subspace of V holds the carrier of W1 c= the carrier of (W1 + W2)
let W1, W2 be Subspace of V; the carrier of W1 c= the carrier of (W1 + W2)
let x be object ; TARSKI:def 3 ( not x in the carrier of W1 or x in the carrier of (W1 + W2) )
assume A1:
x in the carrier of W1
; x in the carrier of (W1 + W2)
the carrier of W1 c= the carrier of V
by RLSUB_1:def 2;
then reconsider w = x as VECTOR of V by A1;
A2:
( w + (0. V) = w & 0. V in W2 )
by RLSUB_1:17;
x in W1
by A1;
then
x in { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 ) }
by A2;
hence
x in the carrier of (W1 + W2)
by RLSUB_2:def 1; verum