let V be RealLinearSpace; :: thesis: for v, u being VECTOR of V
for A being Subset of V st v in Z_Lin A & u in Z_Lin A holds
v + u in Z_Lin A
let v, u be VECTOR of V; :: thesis: for A being Subset of V st v in Z_Lin A & u in Z_Lin A holds
v + u in Z_Lin A
let A be Subset of V; :: thesis: ( v in Z_Lin A & u in Z_Lin A implies v + u in Z_Lin A )
assume that
A2: v in Z_Lin A and
A3: u in Z_Lin A ; :: thesis: v + u in Z_Lin A
consider l1 being Linear_Combination of A such that
A4: ( v = Sum l1 & rng l1 c= INT ) by A2;
consider l2 being Linear_Combination of A such that
A5: ( u = Sum l2 & rng l2 c= INT ) by A3;
reconsider f = l1 + l2 as Linear_Combination of A by RLVECT_2:59;
A6: rng f c= INT by A4, A5, LM001;
v + u = Sum f by A4, A5, RLVECT_3:1;
hence v + u in Z_Lin A by A6; :: thesis: verum