let V be non empty CLSStruct ; :: thesis: for a being Complex
for L being C_Linear_Combination of V st a <> 0c holds
Carrier (a * L) = Carrier L
let a be Complex; :: thesis: for L being C_Linear_Combination of V st a <> 0c holds
Carrier (a * L) = Carrier L
let L be C_Linear_Combination of V; :: thesis: ( a <> 0c implies Carrier (a * L) = Carrier L )
set T = { u where u is VECTOR of V : (a * L) . u <> 0c } ;
set S = { v where v is VECTOR of V : L . v <> 0c } ;
assume A1: a <> 0c ; :: thesis: Carrier (a * L) = Carrier L
{ u where u is VECTOR of V : (a * L) . u <> 0c } = { v where v is VECTOR of V : L . v <> 0c }

proof

thus { u where u is VECTOR of V : (a * L) . u <> 0c } c= { v where v is VECTOR of V : L . v <> 0c } :: according to XBOOLE_0:def 10 :: thesis: { v where v is VECTOR of V : L . v <> 0c } c= { u where u is VECTOR of V : (a * L) . u <> 0c }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { u where u is VECTOR of V : (a * L) . u <> 0c } or x in { v where v is VECTOR of V : L . v <> 0c } )
assume x in { u where u is VECTOR of V : (a * L) . u <> 0c } ; :: thesis: x in { v where v is VECTOR of V : L . v <> 0c }
then consider u being VECTOR of V such that
A2: x = u and
A3: (a * L) . u <> 0c ;
(a * L) . u = a * (L . u) by Def9;
then L . u <> 0c by A3;
hence x in { v where v is VECTOR of V : L . v <> 0c } by A2; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { v where v is VECTOR of V : L . v <> 0c } or x in { u where u is VECTOR of V : (a * L) . u <> 0c } )
assume x in { v where v is VECTOR of V : L . v <> 0c } ; :: thesis: x in { u where u is VECTOR of V : (a * L) . u <> 0c }
then consider v being VECTOR of V such that
A4: ( x = v & L . v <> 0c ) ;
(a * L) . v = a * (L . v) by Def9;
hence x in { u where u is VECTOR of V : (a * L) . u <> 0c } by A1, A4; :: thesis: verum

end;

hence Carrier (a * L) = Carrier L ; :: thesis: verum