theorem :: RLSUB_2:12

for V being strict RealLinearSpace holds ((Omega). V) + ((Omega). V) = V by Th11;