let V be RealLinearSpace; :: thesis: for V', W' being RealLinearSpace st V' = RLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) holds
for W being Subspace of V st W' = RLSStruct(# the carrier of W,the U2 of W,the addF of W,the Mult of W #) holds
W' is Subspace of V'
let V', W' be RealLinearSpace; :: thesis: ( V' = RLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) implies for W being Subspace of V st W' = RLSStruct(# the carrier of W,the U2 of W,the addF of W,the Mult of W #) holds
W' is Subspace of V' )
assume A1: V' = RLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) ; :: thesis: for W being Subspace of V st W' = RLSStruct(# the carrier of W,the U2 of W,the addF of W,the Mult of W #) holds
W' is Subspace of V'
let W be Subspace of V; :: thesis: ( W' = RLSStruct(# the carrier of W,the U2 of W,the addF of W,the Mult of W #) implies W' is Subspace of V' )
assume A2: W' = RLSStruct(# the carrier of W,the U2 of W,the addF of W,the Mult of W #) ; :: thesis: W' is Subspace of V'
hence the carrier of W' c= the carrier of V' by A1, RLSUB_1:def 2; :: according to RLSUB_1:def 2 :: thesis: ( 0. W' = 0. V' & the addF of W' = the addF of V' || the carrier of W' & the Mult of W' = the Mult of V' | [:REAL ,the carrier of W':] )
thus 0. W' = 0. W by A2
.= 0. V by RLSUB_1:def 2
.= 0. V' by A1 ; :: thesis: ( the addF of W' = the addF of V' || the carrier of W' & the Mult of W' = the Mult of V' | [:REAL ,the carrier of W':] )
thus the addF of W' = the addF of V' || the carrier of W' by A1, A2, RLSUB_1:def 2; :: thesis: the Mult of W' = the Mult of V' | [:REAL ,the carrier of W':]
thus the Mult of W' = the Mult of V' | [:REAL ,the carrier of W':] by A1, A2, RLSUB_1:def 2; :: thesis: verum