let V be RealUnitarySpace; for W being strict Subspace of V st ( for v being VECTOR of V holds v in W ) holds
W = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #)
let W be strict Subspace of V; ( ( for v being VECTOR of V holds v in W ) implies W = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) )
assume A1:
for v being VECTOR of V holds v in W
; W = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #)
then
W = (Omega). V
by RUSUB_1:25;
hence
W = 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; verum