let V be 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 Def17;
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 Def17;
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) = K5( 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:95;
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:62;
rng ( the Mult of (RealVS V) | [:REAL, the carrier of (RealVS M):]) c= the carrier of (RealVS M)

proof

let y be object ; :: 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 object 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 3;
consider a, b being object such that
A9: x = [a,b] by A7, RELAT_1:def 1;
reconsider a = a as Element of REAL by A7, A9, ZFMISC_1:87;
reconsider b = b as Element of (RealVS M) by A6, A7, A9, ZFMISC_1:87;
reconsider b1 = b as Element of M by A3;
reconsider b2 = b1 as Element of V by A1;
[[**a,0**],b2] in [: the carrier of F_Complex, the carrier of V:] by ZFMISC_1:87;
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:87;
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:61;
y = the Mult of (RealVS V) . (a,b) by A7, A8, A9, FUNCT_1:47
.= [**a,0**] * b2 by Def17
.= [**a,0**] * b1 by A2, A10, FUNCT_1:47
.= the Mult of (RealVS M) . (a,b) by Def17 ;
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:2;
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) = K5( 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) = K5( the Mult of (RealVS V),[:REAL, the carrier of (RealVS M):])

now :: thesis: for a being Element of REAL
for b being Element of (RealVS M) holds the Mult of (RealVS M) . (a,b) = RM . (a,b)

let a be Element of 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;
[[**a,0**],b2] in [: the carrier of F_Complex, the carrier of V:] by ZFMISC_1:87;
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:87;
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:61;
( a in REAL & b in the carrier of (RealVS V) ) by A5;
then [a,b] in [:REAL, the carrier of (RealVS V):] by ZFMISC_1:87;
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:87;
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:61;
thus the Mult of (RealVS M) . (a,b) = [**a,0**] * b1 by Def17
.= [**a,0**] * b2 by A2, A11, FUNCT_1:47
.= the Mult of (RealVS V) . (a,b) by Def17
.= RM . (a,b) by A12, FUNCT_1:47 ; :: 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