let V be RealUnitarySpace; :: thesis: ( ((0). V) + ((Omega). V) = UNITSTR(# the carrier of V,the ZeroF of V,the U7 of V,the Mult of V,the scalar of V #) & ((Omega). V) + ((0). V) = UNITSTR(# the carrier of V,the ZeroF of V,the U7 of V,the Mult of V,the scalar of V #) )
thus ((0). V) + ((Omega). V) = (Omega). V by Th9
.= UNITSTR(# the carrier of V,the ZeroF of V,the U7 of V,the Mult of V,the scalar of V #) by RUSUB_1:def 3 ; :: thesis: ((Omega). V) + ((0). V) = UNITSTR(# the carrier of V,the ZeroF of V,the U7 of V,the Mult of V,the scalar of V #)
hence ((Omega). V) + ((0). V) = UNITSTR(# the carrier of V,the ZeroF of V,the U7 of V,the Mult of V,the scalar of V #) by Lm1; :: thesis: verum