let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for V being non empty right_complementable VectSp-like Abelian add-associative right_zeroed VectSpStr of GF
for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds
ex W being strict Subspace of V st V1 = the carrier of W
let V be non empty right_complementable VectSp-like Abelian add-associative right_zeroed VectSpStr of GF; :: thesis: for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds
ex W being strict Subspace of V st V1 = the carrier of W
let V1 be Subset of V; :: thesis: ( V1 <> {} & V1 is linearly-closed implies ex W being strict Subspace of V st V1 = the carrier of W )
assume that
A1: V1 <> {} and
A2: V1 is linearly-closed ; :: thesis: ex W being strict Subspace of V st V1 = the carrier of W
reconsider D = V1 as non empty set by A1;
reconsider d = 0. V as Element of D by A2, Th4;
set VV = the carrier of V;
set C = (comp V) | D;
dom (comp V) = the carrier of V by FUNCT_2:def 1;
then A3: dom ((comp V) | D) = D by RELAT_1:91;
A4: rng ((comp V) | D) c= D

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng ((comp V) | D) or x in D )
assume x in rng ((comp V) | D) ; :: thesis: x in D
then consider y being set such that
A5: y in dom ((comp V) | D) and
A6: ((comp V) | D) . y = x by FUNCT_1:def 5;
reconsider y = y as Element of V by A3, A5;
x = (comp V) . y by A5, A6, FUNCT_1:70
.= - y by VECTSP_1:def 25 ;
hence x in D by A2, A3, A5, Th5; :: thesis: verum

end;

set M = the lmult of V | [:the carrier of GF,D:];
dom the lmult of V = [:the carrier of GF,the carrier of V:] by FUNCT_2:def 1;
then A7: dom (the lmult of V | [:the carrier of GF,D:]) = [:the carrier of GF,D:] by RELAT_1:91, ZFMISC_1:119;
A8: rng (the lmult of V | [:the carrier of GF,D:]) c= D

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (the lmult of V | [:the carrier of GF,D:]) or x in D )
assume x in rng (the lmult of V | [:the carrier of GF,D:]) ; :: thesis: x in D
then consider y being set such that
A9: y in dom (the lmult of V | [:the carrier of GF,D:]) and
A10: (the lmult of V | [:the carrier of GF,D:]) . y = x by FUNCT_1:def 5;
consider y1, y2 being set such that
A11: [y1,y2] = y by A7, A9, RELAT_1:def 1;
reconsider y1 = y1 as Element of GF by A7, A9, A11, ZFMISC_1:106;
A12: y2 in V1 by A7, A9, A11, ZFMISC_1:106;
then reconsider y2 = y2 as Element of V ;
x = y1 * y2 by A9, A10, A11, FUNCT_1:70;
hence x in D by A2, A12, Def1; :: thesis: verum

end;

set A = the addF of V || D;
dom the addF of V = [:the carrier of V,the carrier of V:] by FUNCT_2:def 1;
then A13: dom (the addF of V || D) = [:D,D:] by RELAT_1:91, ZFMISC_1:119;
A14: rng (the addF of V || D) c= D

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (the addF of V || D) or x in D )
assume x in rng (the addF of V || D) ; :: thesis: x in D
then consider y being set such that
A15: y in dom (the addF of V || D) and
A16: (the addF of V || D) . y = x by FUNCT_1:def 5;
consider y1, y2 being set such that
A17: [y1,y2] = y by A13, A15, RELAT_1:def 1;
A18: ( y1 in D & y2 in D ) by A13, A15, A17, ZFMISC_1:106;
then reconsider y1 = y1, y2 = y2 as Element of V ;
x = y1 + y2 by A15, A16, A17, FUNCT_1:70;
hence x in D by A2, A18, Def1; :: thesis: verum

end;

reconsider M = the lmult of V | [:the carrier of GF,D:] as Function of [:the carrier of GF,D:],D by A7, A8, FUNCT_2:def 1, RELSET_1:11;
reconsider C = (comp V) | D as UnOp of D by A3, A4, FUNCT_2:def 1, RELSET_1:11;
reconsider A = the addF of V || D as BinOp of D by A13, A14, FUNCT_2:def 1, RELSET_1:11;
set W = VectSpStr(# D,A,d,M #);
A19: for a, b being Element of VectSpStr(# D,A,d,M #)
for x, y being Element of V st x = a & b = y holds
a + b = x + y

proof

let a, b be Element of VectSpStr(# D,A,d,M #); :: thesis: for x, y being Element of V st x = a & b = y holds
a + b = x + y
let x, y be Element of V; :: thesis: ( x = a & b = y implies a + b = x + y )
assume A20: ( x = a & b = y ) ; :: thesis: a + b = x + y
thus a + b = A . [a,b]
.= x + y by A13, A20, FUNCT_1:70 ; :: thesis: verum

end;

A21: ( VectSpStr(# D,A,d,M #) is Abelian & VectSpStr(# D,A,d,M #) is add-associative & VectSpStr(# D,A,d,M #) is right_zeroed & VectSpStr(# D,A,d,M #) is right_complementable )

proof

thus VectSpStr(# D,A,d,M #) is Abelian :: thesis: ( VectSpStr(# D,A,d,M #) is add-associative & VectSpStr(# D,A,d,M #) is right_zeroed & VectSpStr(# D,A,d,M #) is right_complementable )

proof

let a, b be Element of VectSpStr(# D,A,d,M #); :: according to RLVECT_1:def 5 :: thesis: a + b = b + a
reconsider x = a, y = b as Element of V by TARSKI:def 3;
thus a + b = y + x by A19
.= b + a by A19 ; :: thesis: verum

end;

hereby :: according to RLVECT_1:def 6 :: thesis: ( VectSpStr(# D,A,d,M #) is right_zeroed & VectSpStr(# D,A,d,M #) is right_complementable )

let a, b, c be Element of VectSpStr(# D,A,d,M #); :: thesis: (a + b) + c = a + (b + c)
reconsider x = a, y = b, z = c as Element of V by TARSKI:def 3;
A22: b + c = y + z by A19;
a + b = x + y by A19;
hence (a + b) + c = (x + y) + z by A19
.= x + (y + z) by RLVECT_1:def 6
.= a + (b + c) by A19, A22 ;
:: thesis: verum

end;

hereby :: according to RLVECT_1:def 7 :: thesis: VectSpStr(# D,A,d,M #) is right_complementable

let a be Element of VectSpStr(# D,A,d,M #); :: thesis: a + (0. VectSpStr(# D,A,d,M #)) = a
reconsider x = a as Element of V by TARSKI:def 3;
thus a + (0. VectSpStr(# D,A,d,M #)) = x + (0. V) by A19
.= a by RLVECT_1:10 ; :: thesis: verum

end;

let a be Element of VectSpStr(# D,A,d,M #); :: according to ALGSTR_0:def 16 :: thesis: a is right_complementable
reconsider x = a as Element of V by TARSKI:def 3;
reconsider a9 = a as Element of D ;
reconsider b = C . a9 as Element of D ;
reconsider b = b as Element of VectSpStr(# D,A,d,M #) ;
take b ; :: according to ALGSTR_0:def 11 :: thesis: a + b = 0. VectSpStr(# D,A,d,M #)
thus a + b = x + ((comp V) . x) by A3, A19, FUNCT_1:70
.= x + (- x) by VECTSP_1:def 25
.= 0. VectSpStr(# D,A,d,M #) by RLVECT_1:16 ; :: thesis: verum

end;

VectSpStr(# D,A,d,M #) is VectSp-like

proof

let a, b be Element of GF; :: according to VECTSP_1:def 26 :: thesis: for b₁, b₂ being Element of the carrier of VectSpStr(# D,A,d,M #) holds
( a * (b₁ + b₂) = (a * b₁) + (a * b₂) & (a + b) * b₁ = (a * b₁) + (b * b₁) & (a * b) * b₁ = a * (b * b₁) & (1. GF) * b₁ = b₁ )
let v, w be Element of VectSpStr(# D,A,d,M #); :: thesis: ( a * (v + w) = (a * v) + (a * w) & (a + b) * v = (a * v) + (b * v) & (a * b) * v = a * (b * v) & (1. GF) * v = v )
reconsider x = v, y = w as Element of V by TARSKI:def 3;

A23: now

let a be Element of GF; :: thesis: for x being Element of VectSpStr(# D,A,d,M #)
for y being Element of V st y = x holds
a * x = a * y
let x be Element of VectSpStr(# D,A,d,M #); :: thesis: for y being Element of V st y = x holds
a * x = a * y
let y be Element of V; :: thesis: ( y = x implies a * x = a * y )
assume A24: y = x ; :: thesis: a * x = a * y
[a,x] in dom M by A7;
hence a * x = a * y by A24, FUNCT_1:70; :: thesis: verum

end;

then A25: a * v = a * x ;
A26: a * w = a * y by A23;
v + w = x + y by A19;
hence a * (v + w) = a * (x + y) by A23
.= (a * x) + (a * y) by VECTSP_1:def 26
.= (a * v) + (a * w) by A19, A25, A26 ;
:: thesis: ( (a + b) * v = (a * v) + (b * v) & (a * b) * v = a * (b * v) & (1. GF) * v = v )
A27: b * v = b * x by A23;
thus (a + b) * v = (a + b) * x by A23
.= (a * x) + (b * x) by VECTSP_1:def 26
.= (a * v) + (b * v) by A19, A27, A25 ; :: thesis: ( (a * b) * v = a * (b * v) & (1. GF) * v = v )
thus (a * b) * v = (a * b) * x by A23
.= a * (b * x) by VECTSP_1:def 26
.= a * (b * v) by A23, A27 ; :: thesis: (1. GF) * v = v
thus (1. GF) * v = (1_ GF) * x by A23
.= v by VECTSP_1:def 26 ; :: thesis: verum

end;

then reconsider W = VectSpStr(# D,A,d,M #) as non empty right_complementable VectSp-like Abelian add-associative right_zeroed VectSpStr of GF by A21;
0. W = 0. V ;
then reconsider W = W as strict Subspace of V by Def2;
take W ; :: thesis: V1 = the carrier of W
thus V1 = the carrier of W ; :: thesis: verum