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