let V be RealUnitarySpace; :: thesis: for W being Subspace of V holds
( ((Omega). V) + W = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) & W + ((Omega). V) = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) )
let W be Subspace of V; :: thesis: ( ((Omega). V) + W = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) & W + ((Omega). V) = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) )
( the carrier of V = the carrier of UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) & the carrier of W c= the carrier of V ) by RUSUB_1:def 1;
then the carrier of W c= the carrier of ((Omega). V) by RUSUB_1:def 3;
then W + ((Omega). V) = (Omega). V by Lm3
.= 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 ;
hence ( ((Omega). V) + W = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) & W + ((Omega). 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