let V be RealLinearSpace; :: thesis: for a being Real
for A being Subset of V
for L being Linear_Combination of V st L is Linear_Combination of A holds
a * L is Linear_Combination of A
let a be Real; :: thesis: for A being Subset of V
for L being Linear_Combination of V st L is Linear_Combination of A holds
a * L is Linear_Combination of A
let A be Subset of V; :: thesis: for L being Linear_Combination of V st L is Linear_Combination of A holds
a * L is Linear_Combination of A
let L be Linear_Combination of V; :: thesis: ( L is Linear_Combination of A implies a * L is Linear_Combination of A )
assume A1: L is Linear_Combination of A ; :: thesis: a * L is Linear_Combination of A

now :: thesis: a * L is Linear_Combination of A

per cases ( a = 0 or a <> 0 ) ;

suppose a = 0 ; :: thesis: a * L is Linear_Combination of A

then a * L = ZeroLC V by Th43;
hence a * L is Linear_Combination of A by Th22; :: thesis: verum

end;

suppose a <> 0 ; :: thesis: a * L is Linear_Combination of A

then Carrier (a * L) = Carrier L by Th42;
hence a * L is Linear_Combination of A by A1, Def6; :: thesis: verum

end;

end;

end;

hence a * L is Linear_Combination of A ; :: thesis: verum