let V be RealLinearSpace; :: thesis: for X being Subspace of V st V is strict & X is strict & the carrier of X = the carrier of V holds
X = V
let X be Subspace of V; :: thesis: ( V is strict & X is strict & the carrier of X = the carrier of V implies X = V )
assume that
A1: V is strict and
A2: X is strict and
A3: the carrier of X = the carrier of V ; :: thesis: X = V
A4: dom the Mult of V c= [:REAL ,the carrier of V:] ;
A5: the Mult of X = the Mult of V | [:REAL ,the carrier of V:] by A3, RLSUB_1:def 2
.= the Mult of V by A4, RELAT_1:97 ;
A6: 0. X = 0. V by RLSUB_1:def 2;
A7: dom the addF of V c= [:the carrier of V,the carrier of V:] ;
the addF of X = the addF of V || the carrier of V by A3, RLSUB_1:def 2
.= the addF of V | [:the carrier of V,the carrier of V:] by REALSET1:def 3
.= the addF of V by A7, RELAT_1:97 ;
hence X = V by A1, A2, A3, A6, A5; :: thesis: verum