let V be non empty VectSp of F_Complex ; :: thesis: for M being Subspace of V holds RealVS M is Subspace of RealVS V
let M be Subspace of V; :: thesis: RealVS M is Subspace of RealVS V
A1: the carrier of M c= the carrier of V by VECTSP_4:def 2;
A2: the lmult of M = the lmult of V | [:the carrier of F_Complex ,the carrier of M:] by VECTSP_4:def 2;
A3: addLoopStr(# the carrier of M,the addF of M,the ZeroF of M #) = addLoopStr(# the carrier of (RealVS M),the addF of (RealVS M),the ZeroF of (RealVS M) #) by Def22;
A4: addLoopStr(# the carrier of V,the addF of V,the ZeroF of V #) = addLoopStr(# the carrier of (RealVS V),the addF of (RealVS V),the ZeroF of (RealVS V) #) by Def22;
hence A5: the carrier of (RealVS M) c= the carrier of (RealVS V) by A3, VECTSP_4:def 2; :: according to RLSUB_1:def 2 :: thesis: ( 0. (RealVS M) = 0. (RealVS V) & the addF of (RealVS M) = the addF of (RealVS V) || the carrier of (RealVS M) & the Mult of (RealVS M) = K76(the Mult of (RealVS V),[:REAL ,the carrier of (RealVS M):]) )
then [:REAL ,the carrier of (RealVS M):] c= [:REAL ,the carrier of (RealVS V):] by ZFMISC_1:118;
then [:REAL ,the carrier of (RealVS M):] c= dom the Mult of (RealVS V) by FUNCT_2:def 1;
then A6: dom (the Mult of (RealVS V) | [:REAL ,the carrier of (RealVS M):]) = [:REAL ,the carrier of (RealVS M):] by RELAT_1:91;
rng (the Mult of (RealVS V) | [:REAL ,the carrier of (RealVS M):]) c= the carrier of (RealVS M)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (the Mult of (RealVS V) | [:REAL ,the carrier of (RealVS M):]) or y in the carrier of (RealVS M) )
assume y in rng (the Mult of (RealVS V) | [:REAL ,the carrier of (RealVS M):]) ; :: thesis: y in the carrier of (RealVS M)
then consider x being set such that
A7: x in dom (the Mult of (RealVS V) | [:REAL ,the carrier of (RealVS M):]) and
A8: y = (the Mult of (RealVS V) | [:REAL ,the carrier of (RealVS M):]) . x by FUNCT_1:def 5;
consider a, b being set such that
A9: x = [a,b] by A7, RELAT_1:def 1;
reconsider a = a as Real by A7, A9, ZFMISC_1:106;
reconsider b = b as Element of (RealVS M) by A6, A7, A9, ZFMISC_1:106;
reconsider b1 = b as Element of M by A3;
reconsider b2 = b1 as Element of V by A1, TARSKI:def 3;
[[**a,0 **],b2] in [:the carrier of F_Complex ,the carrier of V:] by ZFMISC_1:106;
then ( [[**a,0 **],b1] in [:the carrier of F_Complex ,the carrier of M:] & [[**a,0 **],b2] in dom the lmult of V ) by FUNCT_2:def 1, ZFMISC_1:106;
then [[**a,0 **],b2] in (dom the lmult of V) /\ [:the carrier of F_Complex ,the carrier of M:] by XBOOLE_0:def 4;
then A10: [[**a,0 **],b2] in dom (the lmult of V | [:the carrier of F_Complex ,the carrier of M:]) by RELAT_1:90;
y = the Mult of (RealVS V) . a,b by A7, A8, A9, FUNCT_1:70
.= [**a,0 **] * b2 by Def22
.= [**a,0 **] * b1 by A2, A10, FUNCT_1:70
.= the Mult of (RealVS M) . a,b by Def22 ;
hence y in the carrier of (RealVS M) ; :: thesis: verum

end;

then reconsider RM = the Mult of (RealVS V) | [:REAL ,the carrier of (RealVS M):] as Function of [:REAL ,the carrier of (RealVS M):],the carrier of (RealVS M) by A6, FUNCT_2:4;
thus 0. (RealVS M) = 0. M by A3
.= 0. V by VECTSP_4:def 2
.= 0. (RealVS V) by A4 ; :: thesis: ( the addF of (RealVS M) = the addF of (RealVS V) || the carrier of (RealVS M) & the Mult of (RealVS M) = K76(the Mult of (RealVS V),[:REAL ,the carrier of (RealVS M):]) )
thus the addF of (RealVS M) = the addF of (RealVS V) || the carrier of (RealVS M) by A3, A4, VECTSP_4:def 2; :: thesis: the Mult of (RealVS M) = K76(the Mult of (RealVS V),[:REAL ,the carrier of (RealVS M):])

now

let a be Real; :: thesis: for b being Element of (RealVS M) holds the Mult of (RealVS M) . a,b = RM . a,b
let b be Element of (RealVS M); :: thesis: the Mult of (RealVS M) . a,b = RM . a,b
reconsider b1 = b as Element of M by A3;
reconsider b2 = b1 as Element of V by A1, TARSKI:def 3;
[[**a,0 **],b2] in [:the carrier of F_Complex ,the carrier of V:] by ZFMISC_1:106;
then ( [[**a,0 **],b1] in [:the carrier of F_Complex ,the carrier of M:] & [[**a,0 **],b2] in dom the lmult of V ) by FUNCT_2:def 1, ZFMISC_1:106;
then [[**a,0 **],b2] in (dom the lmult of V) /\ [:the carrier of F_Complex ,the carrier of M:] by XBOOLE_0:def 4;
then A11: [[**a,0 **],b2] in dom (the lmult of V | [:the carrier of F_Complex ,the carrier of M:]) by RELAT_1:90;
b in the carrier of (RealVS V) by A5, TARSKI:def 3;
then [a,b] in [:REAL ,the carrier of (RealVS V):] by ZFMISC_1:106;
then ( [a,b] in [:REAL ,the carrier of (RealVS M):] & [a,b] in dom the Mult of (RealVS V) ) by FUNCT_2:def 1, ZFMISC_1:106;
then [a,b] in (dom the Mult of (RealVS V)) /\ [:REAL ,the carrier of (RealVS M):] by XBOOLE_0:def 4;
then A12: [a,b] in dom RM by RELAT_1:90;
thus the Mult of (RealVS M) . a,b = [**a,0 **] * b1 by Def22
.= [**a,0 **] * b2 by A2, A11, FUNCT_1:70
.= the Mult of (RealVS V) . a,b by Def22
.= RM . a,b by A12, FUNCT_1:70 ; :: thesis: verum

end;

hence the Mult of (RealVS M) = the Mult of (RealVS V) | [:REAL ,the carrier of (RealVS M):] by BINOP_1:2; :: thesis: verum