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