let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; :: thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for a being Element of GF

for L being Linear_Combination of V holds Carrier (a * L) c= Carrier L

let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; :: thesis: for a being Element of GF

for L being Linear_Combination of V holds Carrier (a * L) c= Carrier L

let a be Element of GF; :: thesis: for L being Linear_Combination of V holds Carrier (a * L) c= Carrier L

let L be Linear_Combination of V; :: thesis: Carrier (a * L) c= Carrier L

set T = { u where u is Element of V : (a * L) . u <> 0. GF } ;

set S = { v where v is Element of V : L . v <> 0. GF } ;

{ u where u is Element of V : (a * L) . u <> 0. GF } c= { v where v is Element of V : L . v <> 0. GF }

for a being Element of GF

for L being Linear_Combination of V holds Carrier (a * L) c= Carrier L

let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; :: thesis: for a being Element of GF

for L being Linear_Combination of V holds Carrier (a * L) c= Carrier L

let a be Element of GF; :: thesis: for L being Linear_Combination of V holds Carrier (a * L) c= Carrier L

let L be Linear_Combination of V; :: thesis: Carrier (a * L) c= Carrier L

set T = { u where u is Element of V : (a * L) . u <> 0. GF } ;

set S = { v where v is Element of V : L . v <> 0. GF } ;

{ u where u is Element of V : (a * L) . u <> 0. GF } c= { v where v is Element of V : L . v <> 0. GF }

proof

hence
Carrier (a * L) c= Carrier L
; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { u where u is Element of V : (a * L) . u <> 0. GF } or x in { v where v is Element of V : L . v <> 0. GF } )

assume x in { u where u is Element of V : (a * L) . u <> 0. GF } ; :: thesis: x in { v where v is Element of V : L . v <> 0. GF }

then consider u being Element of V such that

A1: x = u and

A2: (a * L) . u <> 0. GF ;

(a * L) . u = a * (L . u) by Def9;

then L . u <> 0. GF by A2;

hence x in { v where v is Element of V : L . v <> 0. GF } by A1; :: thesis: verum

end;assume x in { u where u is Element of V : (a * L) . u <> 0. GF } ; :: thesis: x in { v where v is Element of V : L . v <> 0. GF }

then consider u being Element of V such that

A1: x = u and

A2: (a * L) . u <> 0. GF ;

(a * L) . u = a * (L . u) by Def9;

then L . u <> 0. GF by A2;

hence x in { v where v is Element of V : L . v <> 0. GF } by A1; :: thesis: verum