let V be strict RealUnitarySpace; :: thesis: for A being Subset of V st A = the carrier of V holds
Lin A = V
let A be Subset of V; :: thesis: ( A = the carrier of V implies Lin A = V )
assume A = the carrier of V ; :: thesis: Lin A = V
then A = the carrier of ((Omega). V) by RUSUB_1:def 3;
hence Lin A = (Omega). V by Th5
.= V by RUSUB_1:def 3 ;
:: thesis: verum