let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; :: thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF
for V1, V2, V3 being Subset of V st V1 is linearly-closed & V2 is linearly-closed & V3 = { (v + u) where v, u is Element of V : ( v in V1 & u in V2 ) } holds
V3 is linearly-closed
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; :: thesis: for V1, V2, V3 being Subset of V st V1 is linearly-closed & V2 is linearly-closed & V3 = { (v + u) where v, u is Element of V : ( v in V1 & u in V2 ) } holds
V3 is linearly-closed
let V1, V2, V3 be Subset of V; :: thesis: ( V1 is linearly-closed & V2 is linearly-closed & V3 = { (v + u) where v, u is Element of V : ( v in V1 & u in V2 ) } implies V3 is linearly-closed )
assume that
A1: ( V1 is linearly-closed & V2 is linearly-closed ) and
A2: V3 = { (v + u) where v, u is Element of V : ( v in V1 & u in V2 ) } ; :: thesis: V3 is linearly-closed
thus for v, u being Element of V st v in V3 & u in V3 holds
v + u in V3 :: according to VECTSP_4:def 1 :: thesis: for a being Element of GF
for v being Element of V st v in V3 holds
a * v in V3

proof

let v, u be Element of V; :: thesis: ( v in V3 & u in V3 implies v + u in V3 )
assume that
A3: v in V3 and
A4: u in V3 ; :: thesis: v + u in V3
consider v1, v2 being Element of V such that
A5: v = v1 + v2 and
A6: ( v1 in V1 & v2 in V2 ) by A2, A3;
consider u1, u2 being Element of V such that
A7: u = u1 + u2 and
A8: ( u1 in V1 & u2 in V2 ) by A2, A4;
A9: v + u = ((v1 + v2) + u1) + u2 by A5, A7, RLVECT_1:def 3
.= ((v1 + u1) + v2) + u2 by RLVECT_1:def 3
.= (v1 + u1) + (v2 + u2) by RLVECT_1:def 3 ;
( v1 + u1 in V1 & v2 + u2 in V2 ) by A1, A6, A8;
hence v + u in V3 by A2, A9; :: thesis: verum

end;

let a be Element of GF; :: thesis: for v being Element of V st v in V3 holds
a * v in V3
let v be Element of V; :: thesis: ( v in V3 implies a * v in V3 )
assume v in V3 ; :: thesis: a * v in V3
then consider v1, v2 being Element of V such that
A10: v = v1 + v2 and
A11: ( v1 in V1 & v2 in V2 ) by A2;
A12: a * v = (a * v1) + (a * v2) by A10, VECTSP_1:def 14;
( a * v1 in V1 & a * v2 in V2 ) by A1, A11;
hence a * v in V3 by A2, A12; :: thesis: verum