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

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

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 a be Element of GF; :: thesis: for v being Element of V st v in V3 holds
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;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

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