theorem Th72: :: REAL_NS2:72

for T being RealLinearSpace
for X being set holds
( X is Linear_Combination of RLSp2RVSp T iff X is Linear_Combination of T )