let R be Ring; :: thesis: for V being RightMod of R
for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds
ex W being strict Submodule of V st V1 = the carrier of W
let V be RightMod of R; :: thesis: for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds
ex W being strict Submodule 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 Submodule of V st V1 = the carrier of W )
assume that
A1: V1 <> {} and
A2: V1 is linearly-closed ; :: thesis: ex W being strict Submodule of V st V1 = the carrier of W
set VV = the carrier of V;
reconsider D = V1 as non empty set by A1;
set A = the addF of V || D;
( V1 c= 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 || D) = [:D,D:] by RELAT_1:91, ZFMISC_1:119;
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
A4: y in dom (the addF of V || D) and
A5: (the addF of V || D) . y = x by FUNCT_1:def 5;
consider y1, y2 being set such that
A6: [y1,y2] = y by A3, A4, RELAT_1:def 1;
A7: ( y1 in D & y2 in D & D c= the carrier of V ) by A3, A4, A6, ZFMISC_1:106;
then reconsider y1 = y1, y2 = y2 as Vector of V ;
x = y1 + y2 by A4, A5, A6, FUNCT_1:70;
hence x in D by A2, A7, Def1; :: thesis: verum

end;

then reconsider A = the addF of V || D as BinOp of D by A3, FUNCT_2:def 1, RELSET_1:11;
set C = (comp V) | D;
( V1 c= the carrier of V & dom (comp V) = the carrier of V ) by FUNCT_2:def 1;
then A8: dom ((comp V) | D) = D by RELAT_1:91;
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
A9: y in dom ((comp V) | D) and
A10: ((comp V) | D) . y = x by FUNCT_1:def 5;
reconsider y = y as Vector of V by A8, A9;
x = (comp V) . y by A9, A10, FUNCT_1:70
.= - y by VECTSP_1:def 25 ;
hence x in D by A2, A8, A9, Th5; :: thesis: verum

end;

then reconsider C = (comp V) | D as UnOp of D by A8, FUNCT_2:def 1, RELSET_1:11;
set M = the rmult of V | [:D,the carrier of R:];
reconsider d = 0. V as Element of D by A2, Th4;
dom the rmult of V = [:the carrier of V,the carrier of R:] by FUNCT_2:def 1;
then A11: dom (the rmult of V | [:D,the carrier of R:]) = [:D,the carrier of R:] by RELAT_1:91, ZFMISC_1:119;
rng (the rmult of V | [:D,the carrier of R:]) c= D

proof

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

end;

then reconsider M = the rmult of V | [:D,the carrier of R:] as Function of [:D,the carrier of R:],D by A11, FUNCT_2:def 1, RELSET_1:11;
set W = RightModStr(# D,A,d,M #);
A16: for a, b being Element of RightModStr(# D,A,d,M #)
for x, y being Vector of V st x = a & b = y holds
a + b = x + y

proof

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

end;

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

proof

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

proof

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

end;

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

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

end;

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

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

end;

let a be Element of RightModStr(# D,A,d,M #); :: according to ALGSTR_0:def 16 :: thesis: a is right_complementable
reconsider x = a as Vector of V by TARSKI:def 3;
reconsider b' = (comp V) . x as Vector of V ;
C . x in D by FUNCT_2:7;
then reconsider b = ((comp V) | D) . x as Element of RightModStr(# D,A,d,M #) ;
take b ; :: according to ALGSTR_0:def 11 :: thesis: a + b = 0. RightModStr(# D,A,d,M #)
thus a + b = x + b' by A16, FUNCT_1:72
.= x + (- x) by VECTSP_1:def 25
.= 0. RightModStr(# D,A,d,M #) by RLVECT_1:16 ; :: thesis: verum

end;

RightModStr(# D,A,d,M #) is RightMod-like

proof

let a, b be Scalar of R; :: according to VECTSP_2:def 23 :: thesis: for b₁, b₂ being Element of the carrier of RightModStr(# D,A,d,M #) holds
( (b₁ + b₂) * a = (b₁ * a) + (b₂ * a) & b₁ * (a + b) = (b₁ * a) + (b₁ * b) & b₁ * (b * a) = (b₁ * b) * a & b₁ * (1_ R) = b₁ )
let v, w be Vector of RightModStr(# D,A,d,M #); :: thesis: ( (v + w) * a = (v * a) + (w * a) & v * (a + b) = (v * a) + (v * b) & v * (b * a) = (v * b) * a & v * (1_ R) = v )
reconsider x = v, y = w as Vector of V by TARSKI:def 3;

A20: now

let a be Scalar of R; :: thesis: for x being Element of RightModStr(# D,A,d,M #)
for y being Vector of V st y = x holds
x * a = y * a
let x be Element of RightModStr(# D,A,d,M #); :: thesis: for y being Vector of V st y = x holds
x * a = y * a
let y be Vector of V; :: thesis: ( y = x implies x * a = y * a )
assume A21: y = x ; :: thesis: x * a = y * a
[x,a] in dom M by A11;
hence x * a = y * a by A21, FUNCT_1:70; :: thesis: verum

end;

then A22: ( v * b = x * b & v * a = x * a & w * a = y * a ) ;
then ( (v * a) + (w * a) = (x * a) + (y * a) & v + w = x + y ) by A16;
hence (v + w) * a = (x + y) * a by A20
.= (x * a) + (y * a) by VECTSP_2:def 23
.= (v * a) + (w * a) by A16, A22 ;
:: thesis: ( v * (a + b) = (v * a) + (v * b) & v * (b * a) = (v * b) * a & v * (1_ R) = v )
thus v * (a + b) = x * (a + b) by A20
.= (x * a) + (x * b) by VECTSP_2:def 23
.= (v * a) + (v * b) by A16, A22 ; :: thesis: ( v * (b * a) = (v * b) * a & v * (1_ R) = v )
thus v * (b * a) = x * (b * a) by A20
.= (x * b) * a by VECTSP_2:def 23
.= (v * b) * a by A20, A22 ; :: thesis: v * (1_ R) = v
thus v * (1_ R) = x * (1_ R) by A20
.= v by VECTSP_2:def 23 ; :: thesis: verum

end;

then reconsider W = RightModStr(# D,A,d,M #) as RightMod of R by A18;
0. W = 0. V ;
then reconsider W = W as strict Submodule of V by Def2;
take W ; :: thesis: V1 = the carrier of W
thus V1 = the carrier of W ; :: thesis: verum