let V be strict RealLinearSpace; :: 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) ;

hence Lin A = V by Th18; :: thesis: verum

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) ;

hence Lin A = V by Th18; :: thesis: verum