let V be RealLinearSpace; :: thesis: for W1 being Subspace of V

for W2 being strict Subspace of V st the carrier of W1 c= the carrier of W2 holds

W1 + W2 = W2

let W1 be Subspace of V; :: thesis: for W2 being strict Subspace of V st the carrier of W1 c= the carrier of W2 holds

W1 + W2 = W2

let W2 be strict Subspace of V; :: thesis: ( the carrier of W1 c= the carrier of W2 implies W1 + W2 = W2 )

assume A1: the carrier of W1 c= the carrier of W2 ; :: thesis: W1 + W2 = W2

A2: the carrier of (W1 + W2) c= the carrier of W2

then the carrier of W2 c= the carrier of (W1 + W2) by Lm2;

then the carrier of (W1 + W2) = the carrier of W2 by A2;

hence W1 + W2 = W2 by RLSUB_1:30; :: thesis: verum

for W2 being strict Subspace of V st the carrier of W1 c= the carrier of W2 holds

W1 + W2 = W2

let W1 be Subspace of V; :: thesis: for W2 being strict Subspace of V st the carrier of W1 c= the carrier of W2 holds

W1 + W2 = W2

let W2 be strict Subspace of V; :: thesis: ( the carrier of W1 c= the carrier of W2 implies W1 + W2 = W2 )

assume A1: the carrier of W1 c= the carrier of W2 ; :: thesis: W1 + W2 = W2

A2: the carrier of (W1 + W2) c= the carrier of W2

proof

W1 + W2 = W2 + W1
by Lm1;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (W1 + W2) or x in the carrier of W2 )

assume x in the carrier of (W1 + W2) ; :: thesis: x in the carrier of W2

then x in { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 ) } by Def1;

then consider u, v being VECTOR of V such that

A3: x = v + u and

A4: v in W1 and

A5: u in W2 ;

W1 is Subspace of W2 by A1, RLSUB_1:28;

then v in W2 by A4, RLSUB_1:8;

then v + u in W2 by A5, RLSUB_1:20;

hence x in the carrier of W2 by A3, STRUCT_0:def 5; :: thesis: verum

end;assume x in the carrier of (W1 + W2) ; :: thesis: x in the carrier of W2

then x in { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 ) } by Def1;

then consider u, v being VECTOR of V such that

A3: x = v + u and

A4: v in W1 and

A5: u in W2 ;

W1 is Subspace of W2 by A1, RLSUB_1:28;

then v in W2 by A4, RLSUB_1:8;

then v + u in W2 by A5, RLSUB_1:20;

hence x in the carrier of W2 by A3, STRUCT_0:def 5; :: thesis: verum

then the carrier of W2 c= the carrier of (W1 + W2) by Lm2;

then the carrier of (W1 + W2) = the carrier of W2 by A2;

hence W1 + W2 = W2 by RLSUB_1:30; :: thesis: verum