theorem Th33: :: IDEAL_1:33

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