let V be ComplexLinearSpace; :: thesis: for V1, V2, V3 being Subset of V st V1 is linearly-closed & V2 is linearly-closed & V3 = { (v + u) where u, v is VECTOR 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 u, v is VECTOR 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 u, v is VECTOR of V : ( v in V1 & u in V2 ) } ; :: thesis: V3 is linearly-closed
thus for v, u being VECTOR of V st v in V3 & u in V3 holds
v + u in V3 :: according to CLVECT_1:def 7 :: thesis: for z being Complex
for v being VECTOR of V st v in V3 holds
z * v in V3

proof

let v, u be VECTOR 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 v2, v1 being VECTOR of V such that
A5: v = v1 + v2 and
A6: ( v1 in V1 & v2 in V2 ) by A2, A3;
consider u2, u1 being VECTOR 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 z be Complex; :: thesis: for v being VECTOR of V st v in V3 holds
z * v in V3
let v be VECTOR of V; :: thesis: ( v in V3 implies z * v in V3 )
assume v in V3 ; :: thesis: z * v in V3
then consider v2, v1 being VECTOR of V such that
A10: v = v1 + v2 and
A11: ( v1 in V1 & v2 in V2 ) by A2;
A12: z * v = (z * v1) + (z * v2) by A10, Def2;
( z * v1 in V1 & z * v2 in V2 ) by A1, A11;
hence z * v in V3 by A2, A12; :: thesis: verum