let V be Z_Module; :: thesis: for L being Z_Linear_Combination of V
for a being Integer
for A being Subset of V st L is Z_Linear_Combination of A holds
a * L is Z_Linear_Combination of A
let L be Z_Linear_Combination of V; :: thesis: for a being Integer
for A being Subset of V st L is Z_Linear_Combination of A holds
a * L is Z_Linear_Combination of A
let a be Integer; :: thesis: for A being Subset of V st L is Z_Linear_Combination of A holds
a * L is Z_Linear_Combination of A
let A be Subset of V; :: thesis: ( L is Z_Linear_Combination of A implies a * L is Z_Linear_Combination of A )
assume A1: L is Z_Linear_Combination of A ; :: thesis: a * L is Z_Linear_Combination of A

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

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

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

then a * L = Z_ZeroLC V by Th30;
hence a * L is Z_Linear_Combination of A by Th11; :: thesis: verum

end;

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

then Carrier (a * L) = Carrier L by Th29;
hence a * L is Z_Linear_Combination of A by A1, Def21; :: thesis: verum

end;

end;

end;

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