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 A1: ( V is strict & X is strict & the carrier of X = the carrier of V ) ; :: thesis: X = V
A2: ( the carrier of X c= the carrier of V & 0. X = 0. V & the addF of X = the addF of V || the carrier of X & the Mult of X = the Mult of V | [:REAL ,the carrier of X:] ) by RLSUB_1:def 2;
A3: dom the addF of V c= [:the carrier of V,the carrier of V:] ;
A4: the addF of X = the addF of V || the carrier of V by A1, 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 A3, RELAT_1:97 ;
A5: dom the Mult of V c= [:REAL ,the carrier of V:] ;
the Mult of X = the Mult of V | [:REAL ,the carrier of V:] by A1, RLSUB_1:def 2
.= the Mult of V by A5, RELAT_1:97 ;
hence X = V by A1, A2, A4; :: thesis: verum