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
A1: v in Z_Lin A and
A2: u in Z_Lin A ; :: thesis: v + u in Z_Lin A
consider l1 being Linear_Combination of A such that
A3: ( v = Sum l1 & rng l1 c= INT ) by A1;
consider l2 being Linear_Combination of A such that
A4: ( u = Sum l2 & rng l2 c= INT ) by A2;
reconsider f = l1 + l2 as Linear_Combination of A by RLVECT_2:38;
A5: rng f c= INT by A3, A4, Th5;
v + u = Sum f by A3, A4, RLVECT_3:1;
hence v + u in Z_Lin A by A5; :: thesis: verum