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