theorem Th34: :: IDEAL_1:34

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