let V be RealUnitarySpace; :: thesis:
let V1 be Subset of V; :: thesis:
assume that
A1: V1 <> {} and
A2: V1 is linearly-closed ; :: thesis:
reconsider D = V1 as non empty set by A1;
reconsider d1 = 0. V as Element of D by A2, RLSUB_1:4;
set A = the addF of V || V1;
set M = the Mult of V | [:REAL ,V1:];
set S = the scalar of V || V1;
set VV = the carrier of V;
dom the addF of V = [:the carrier of V,the carrier of V:] by FUNCT_2:def 1;
then A3: ( dom (the addF of V || V1) = [:the carrier of V,the carrier of V:] /\ [:V1,V1:] & [:V1,V1:] c= [:the carrier of V,the carrier of V:] ) by RELAT_1:90;
then A4: dom (the addF of V || V1) = [:D,D:] by XBOOLE_1:28;
dom the Mult of V = [:REAL ,the carrier of V:] by FUNCT_2:def 1;
then ( dom (the Mult of V | [:REAL ,V1:]) = [:REAL ,the carrier of V:] /\ [:REAL ,V1:] & [:REAL ,V1:] c= [:REAL ,the carrier of V:] ) by RELAT_1:90, ZFMISC_1:118;
then A5: dom (the Mult of V | [:REAL ,V1:]) = [:REAL ,D:] by XBOOLE_1:28;
A6: D = rng (the addF of V || V1)

let y be set ; :: thesis:
thus ( y in D implies ex x being set st
( x in dom (the addF of V || V1) & y = (the addF of V || V1) . x ) ) :: thesis:

assume A7: y in D ; :: thesis:
then reconsider v1 = y, v0 = d1 as Element of the carrier of V ;
A8: ( [d1,y] in [:D,D:] & [d1,y] in [:the carrier of V,the carrier of V:] ) by A7, ZFMISC_1:106;
then (the addF of V || V1) . [d1,y] = v0 + v1 by FUNCT_1:72
.= y by RLVECT_1:10 ;
hence ex x being set st
( x in dom (the addF of V || V1) & y = (the addF of V || V1) . x ) by A4, A8; :: thesis:

end;

given x being set such that A9: x in dom (the addF of V || V1) and
A10: y = (the addF of V || V1) . x ; :: thesis:
consider x1, x2 being set such that
A11: ( x1 in D & x2 in D ) and
A12: x = [x1,x2] by A4, A9, ZFMISC_1:def 2;
A13: ( [x1,x2] in [:the carrier of V,the carrier of V:] & [x1,x2] in [:V1,V1:] ) by A11, ZFMISC_1:106;
reconsider v1 = x1, v2 = x2 as Element of the carrier of V by A11;
y = v1 + v2 by A10, A12, A13, FUNCT_1:72;
hence y in D by A2, A11, RLSUB_1:def 1; :: thesis:

end;

hence D = rng (the addF of V || V1) by FUNCT_1:def 5; :: thesis:

end;

A14: D = rng (the Mult of V | [:REAL ,V1:])

let y be set ; :: thesis:
thus ( y in D implies ex x being set st
( x in dom (the Mult of V | [:REAL ,V1:]) & y = (the Mult of V | [:REAL ,V1:]) . x ) ) :: thesis:

assume A15: y in D ; :: thesis:
then reconsider v1 = y as Element of the carrier of V ;
A16: ( [1,y] in [:REAL ,D:] & [1,y] in [:REAL ,the carrier of V:] ) by A15, ZFMISC_1:106;
then (the Mult of V | [:REAL ,V1:]) . [1,y] = 1 * v1 by FUNCT_1:72
.= y by RLVECT_1:def 9 ;
hence ex x being set st
( x in dom (the Mult of V | [:REAL ,V1:]) & y = (the Mult of V | [:REAL ,V1:]) . x ) by A5, A16; :: thesis:

end;

given x being set such that A17: x in dom (the Mult of V | [:REAL ,V1:]) and
A18: y = (the Mult of V | [:REAL ,V1:]) . x ; :: thesis:
consider x1, x2 being set such that
A19: x1 in REAL and
A20: x2 in D and
A21: x = [x1,x2] by A5, A17, ZFMISC_1:def 2;
A22: ( [x1,x2] in [:REAL ,the carrier of V:] & [x1,x2] in [:REAL ,V1:] ) by A19, A20, ZFMISC_1:106;
reconsider v2 = x2 as Element of the carrier of V by A20;
reconsider xx1 = x1 as Real by A19;
y = xx1 * v2 by A18, A21, A22, FUNCT_1:72;
hence y in D by A2, A20, RLSUB_1:def 1; :: thesis:

end;

hence D = rng (the Mult of V | [:REAL ,V1:]) by FUNCT_1:def 5; :: thesis:

end;

reconsider A = the addF of V || V1 as Function of [:D,D:],D by A4, A6, FUNCT_2:def 1, RELSET_1:11;
reconsider M = the Mult of V | [:REAL ,V1:] as Function of [:REAL ,D:],D by A5, A14, FUNCT_2:def 1, RELSET_1:11;
reconsider S = the scalar of V || V1 as Function of [:D,D:],REAL by A3, FUNCT_2:38;
set W = UNITSTR(# D,d1,A,M,S #);
( UNITSTR(# D,d1,A,M,S #) is Subspace of V & the carrier of UNITSTR(# D,d1,A,M,S #) = D ) by Th18;
hence ex W being strict Subspace of V st V1 = the carrier of W ; :: thesis: