let R be non empty associative multLoopStr ; :: thesis: for A being non empty Subset of R
for a being Element of R
for F being LeftLinearCombination of A holds a * F is LeftLinearCombination of A
let A be non empty Subset of R; :: thesis: for a being Element of R
for F being LeftLinearCombination of A holds a * F is LeftLinearCombination of A
let a be Element of R; :: thesis: for F being LeftLinearCombination of A holds a * F is LeftLinearCombination of A
let F be LeftLinearCombination of A; :: thesis: a * F is LeftLinearCombination of A
let i be set ; :: according to IDEAL_1:def 9 :: thesis: ( i in dom (a * F) implies ex u being Element of R ex a being Element of A st (a * F) /. i = u * a )
assume i in dom (a * F) ; :: thesis: ex u being Element of R ex a being Element of A st (a * F) /. i = u * a
then A1: i in dom F by POLYNOM1:def 1;
then consider u being Element of R, b being Element of A such that
A2: F /. i = u * b by Def9;
take x = a * u; :: thesis: ex a being Element of A st (a * F) /. i = x * a
take b ; :: thesis: (a * F) /. i = x * b
thus (a * F) /. i = a * (F /. i) by A1, POLYNOM1:def 1
.= x * b by A2, GROUP_1:def 3 ; :: thesis: verum