theorem Th32: :: IDEAL_1:32

for S being non empty doubleLoopStr
for F being non empty Subset of S
for lc being non empty LinearCombination of F ex p being LinearCombination of F ex e being Element of S st
( lc = p ^ <*e*> & <*e*> is LinearCombination of F )