let V be RealUnitarySpace; :: thesis: 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; :: thesis: ( ( 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 ; :: thesis: W = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #)
now :: thesis: for v being VECTOR of V holds
( ( v in W implies v in (Omega). V ) & ( v in (Omega). V implies v in W ) )
let v be VECTOR of V; :: thesis: ( ( v in W implies v in (Omega). V ) & ( v in (Omega). V implies v in W ) )
thus ( v in W implies v in (Omega). V ) :: thesis: ( v in (Omega). V implies v in W )
proof
assume v in W ; :: thesis: v in (Omega). V
v in UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) by RLVECT_1:1;
hence v in (Omega). V by RUSUB_1:def 3; :: thesis: verum
end;
assume v in (Omega). V ; :: thesis: v in W
thus v in W by A1; :: thesis: verum
end;
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; :: thesis: verum