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: addLoopStr(# the carrier of M,the addF of M,the U2 of M #) = addLoopStr(# the carrier of (RealVS M),the addF of (RealVS M),the U2 of (RealVS M) #) by Def22;
A3: addLoopStr(# the carrier of V,the addF of V,the U2 of V #) = addLoopStr(# the carrier of (RealVS V),the addF of (RealVS V),the U2 of (RealVS V) #) by Def22;
hence A4: the carrier of (RealVS M) c= the carrier of (RealVS V) by A2, 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) = K7(the Mult of (RealVS V),[:REAL ,the carrier of (RealVS M):]) )
thus 0. (RealVS M) = 0. M by A2
.= 0. V by VECTSP_4:def 2
.= 0. (RealVS V) by A3 ; :: thesis: ( the addF of (RealVS M) = the addF of (RealVS V) || the carrier of (RealVS M) & the Mult of (RealVS M) = K7(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 A2, A3, VECTSP_4:def 2; :: thesis: the Mult of (RealVS M) = K7(the Mult of (RealVS V),[:REAL ,the carrier of (RealVS M):])
[:REAL ,the carrier of (RealVS M):] c= [:REAL ,the carrier of (RealVS V):] by A4, ZFMISC_1:118;
then [:REAL ,the carrier of (RealVS M):] c= dom the Mult of (RealVS V) by FUNCT_2:def 1;
then A5: dom (the Mult of (RealVS V) | [:REAL ,the carrier of (RealVS M):]) = [:REAL ,the carrier of (RealVS M):] by RELAT_1:91;
A6: the lmult of M = the lmult of V | [:the carrier of F_Complex ,the carrier of M:] by VECTSP_4:def 2;
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 A5, A7, A9, ZFMISC_1:106;
reconsider b1 = b as Element of M by A2;
reconsider b2 = b1 as Element of V by A1, TARSKI:def 3;
A10: [[**a,0 **],b1] in [:the carrier of F_Complex ,the carrier of M:] by ZFMISC_1:106;
[[**a,0 **],b2] in [:the carrier of F_Complex ,the carrier of V:] by ZFMISC_1:106;
then [[**a,0 **],b2] in dom the lmult of V by FUNCT_2:def 1;
then [[**a,0 **],b2] in (dom the lmult of V) /\ [:the carrier of F_Complex ,the carrier of M:] by A10, 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;
y = the Mult of (RealVS V) . a,b by A7, A8, A9, FUNCT_1:70
.= [**a,0 **] * b2 by Def22
.= [**a,0 **] * b1 by A6, A11, 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 A5, FUNCT_2:4;

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 A2;
reconsider b2 = b1 as Element of V by A1, TARSKI:def 3;
A12: [a,b] in [:REAL ,the carrier of (RealVS M):] by ZFMISC_1:106;
b in the carrier of (RealVS V) by A4, TARSKI:def 3;
then [a,b] in [:REAL ,the carrier of (RealVS V):] by ZFMISC_1:106;
then [a,b] in dom the Mult of (RealVS V) by FUNCT_2:def 1;
then [a,b] in (dom the Mult of (RealVS V)) /\ [:REAL ,the carrier of (RealVS M):] by A12, XBOOLE_0:def 4;
then A13: [a,b] in dom RM by RELAT_1:90;
A14: [[**a,0 **],b1] in [:the carrier of F_Complex ,the carrier of M:] by ZFMISC_1:106;
[[**a,0 **],b2] in [:the carrier of F_Complex ,the carrier of V:] by ZFMISC_1:106;
then [[**a,0 **],b2] in dom the lmult of V by FUNCT_2:def 1;
then [[**a,0 **],b2] in (dom the lmult of V) /\ [:the carrier of F_Complex ,the carrier of M:] by A14, XBOOLE_0:def 4;
then A15: [[**a,0 **],b2] in dom (the lmult of V | [:the carrier of F_Complex ,the carrier of M:]) by RELAT_1:90;
thus the Mult of (RealVS M) . a,b = [**a,0 **] * b1 by Def22
.= [**a,0 **] * b2 by A6, A15, FUNCT_1:70
.= the Mult of (RealVS V) . a,b by Def22
.= RM . a,b by A13, 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