:: LMOD_6 semantic presentation

begin


notation
let K be Ring;
let V be LeftMod of K;
synonym  Submodules V for  Subspaces V;
end;

theorem :: LMOD_6:1
for x being set
for K being Ring
for M1, M2 being LeftMod of K st M1 = VectSpStr(# the carrier of M2, the addF of M2, the ZeroF of M2, the lmult of M2 #) holds
( x in M1 iff x in M2 )
proof
let x be set ; ::_thesis: for K being Ring
for M1, M2 being LeftMod of K st M1 = VectSpStr(# the carrier of M2, the addF of M2, the ZeroF of M2, the lmult of M2 #) holds
( x in M1 iff x in M2 )
let K be Ring; ::_thesis: for M1, M2 being LeftMod of K st M1 = VectSpStr(# the carrier of M2, the addF of M2, the ZeroF of M2, the lmult of M2 #) holds
( x in M1 iff x in M2 )
let M1, M2 be LeftMod of K; ::_thesis: ( M1 = VectSpStr(# the carrier of M2, the addF of M2, the ZeroF of M2, the lmult of M2 #) implies ( x in M1 iff x in M2 ) )
A1: ( x in M1 iff x in the carrier of M1 ) by STRUCT_0:def_5;
assume  M1 = VectSpStr(# the carrier of M2, the addF of M2, the ZeroF of M2, the lmult of M2 #) ; ::_thesis: ( x in M1 iff x in M2 )
hence  ( x in M1 iff x in M2 ) by A1, STRUCT_0:def_5; ::_thesis: verum
end;

theorem :: LMOD_6:2
for K being Ring
for r being Scalar of K
for V being LeftMod of K
for a being Vector of V
for v being Vector of VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) st a = v holds
r * a = r * v
proof
let K be Ring; ::_thesis: for r being Scalar of K
for V being LeftMod of K
for a being Vector of V
for v being Vector of VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) st a = v holds
r * a = r * v
let r be Scalar of K; ::_thesis: for V being LeftMod of K
for a being Vector of V
for v being Vector of VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) st a = v holds
r * a = r * v
let V be LeftMod of K; ::_thesis: for a being Vector of V
for v being Vector of VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) st a = v holds
r * a = r * v
let a be Vector of V; ::_thesis: for v being Vector of VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) st a = v holds
r * a = r * v
let v be Vector of VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #); ::_thesis: ( a = v implies r * a = r * v )
assume A1: a = v ; ::_thesis: r * a = r * v
thus r * a = the lmult of V . (r,a) by VECTSP_1:def_12
.= r * v by A1, VECTSP_1:def_12 ; ::_thesis: verum
end;

theorem Th3: :: LMOD_6:3
for K being Ring
for V being LeftMod of K holds VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is strict Subspace of V
proof
let K be Ring; ::_thesis: for V being LeftMod of K holds VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is strict Subspace of V
let V be LeftMod of K; ::_thesis: VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is strict Subspace of V
 (Omega). V = VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) by VECTSP_4:def_4;
hence  VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is strict Subspace of V ; ::_thesis: verum
end;

theorem Th4: :: LMOD_6:4
for K being Ring
for V being LeftMod of K holds V is Subspace of (Omega). V
proof
let K be Ring; ::_thesis: for V being LeftMod of K holds V is Subspace of (Omega). V
let V be LeftMod of K; ::_thesis: V is Subspace of (Omega). V
set W = (Omega). V;
A1: (Omega). V = VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) by VECTSP_4:def_4;
then A2: 0. V = 0. ((Omega). V) ;
 dom the lmult of ((Omega). V) = [: the carrier of K, the carrier of ((Omega). V):] by FUNCT_2:def_1;
then A3: the lmult of V = the lmult of ((Omega). V) | [: the carrier of K, the carrier of V:] by A1, RELAT_1:68;
 dom the addF of ((Omega). V) = [: the carrier of ((Omega). V), the carrier of ((Omega). V):] by FUNCT_2:def_1;
then  the addF of V = the addF of ((Omega). V) || the carrier of V by A1, RELAT_1:68;
hence  V is Subspace of (Omega). V by A1, A2, A3, VECTSP_4:def_2; ::_thesis: verum
end;

begin

definition
let K be Ring;
redefine attr K is trivial  means :Def1: :: LMOD_6:def 1
 0. K = 1_ K;
compatibility
 ( K is trivial iff 0. K = 1_ K )
proof
thus  ( K is trivial implies 0. K = 1_ K ) by STRUCT_0:def_18; ::_thesis: ( 0. K = 1_ K implies K is trivial )
assume A1: 0. K = 1_ K ; ::_thesis: K is trivial
now__::_thesis:_for_x_being_Scalar_of_K_holds_x_=_0._K
let x be Scalar of K; ::_thesis: x = 0. K
thus x = x * (1_ K) by VECTSP_1:def_4
.= 0. K by A1, VECTSP_1:6 ; ::_thesis: verum
end;
hence  K is trivial by STRUCT_0:def_18; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines trivial LMOD_6:def_1_:_
 for K being Ring holds
( K is trivial iff 0. K = 1_ K );

theorem Th5: :: LMOD_6:5
for K being Ring
for V being LeftMod of K st K is trivial holds
( ( for r being Scalar of K holds r = 0. K ) & ( for a being Vector of V holds a = 0. V ) )
proof
let K be Ring; ::_thesis: for V being LeftMod of K st K is trivial holds
( ( for r being Scalar of K holds r = 0. K ) & ( for a being Vector of V holds a = 0. V ) )
let V be LeftMod of K; ::_thesis: ( K is trivial implies ( ( for r being Scalar of K holds r = 0. K ) & ( for a being Vector of V holds a = 0. V ) ) )
assume  K is trivial ; ::_thesis: ( ( for r being Scalar of K holds r = 0. K ) & ( for a being Vector of V holds a = 0. V ) )
then A1: 0. K = 1_ K by Def1;
A2: now__::_thesis:_for_a_being_Vector_of_V_holds_a_=_0._V
let a be Vector of V; ::_thesis: a = 0. V
thus a = (1_ K) * a by VECTSP_1:def_17
.= 0. V by A1, VECTSP_1:14 ; ::_thesis: verum
end;
now__::_thesis:_for_r_being_Scalar_of_K_holds_r_=_0._K
let r be Scalar of K; ::_thesis: r = 0. K
thus r = r * (1_ K) by VECTSP_1:def_4
.= 0. K by A1, VECTSP_1:6 ; ::_thesis: verum
end;
hence  ( ( for r being Scalar of K holds r = 0. K ) & ( for a being Vector of V holds a = 0. V ) ) by A2; ::_thesis: verum
end;

theorem :: LMOD_6:6
for K being Ring
for V being LeftMod of K st K is trivial holds
V is trivial
proof
let K be Ring; ::_thesis: for V being LeftMod of K st K is trivial holds
V is trivial
let V be LeftMod of K; ::_thesis: ( K is trivial implies V is trivial )
assume that
A1: K is trivial and
A2: not V is trivial ; ::_thesis: contradiction
 ex a being Vector of V st a <> 0. V by A2, STRUCT_0:def_18;
hence  contradiction by A1, Th5; ::_thesis: verum
end;

theorem :: LMOD_6:7
for K being Ring
for V being LeftMod of K holds
( V is trivial iff VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) = (0). V )
proof
let K be Ring; ::_thesis: for V being LeftMod of K holds
( V is trivial iff VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) = (0). V )
let V be LeftMod of K; ::_thesis: ( V is trivial iff VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) = (0). V )
set X = the carrier of ((0). V);
reconsider W = VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) as strict Subspace of V by Th3;
reconsider Z = (0). V as Subspace of W by VECTSP_4:39;
A1: now__::_thesis:_(_W_<>_Z_implies_not_V_is_trivial_)
assume  W <> Z ; ::_thesis: not V is trivial
then consider a being Vector of V such that
A2: not a in Z by VECTSP_4:32;
 not a in the carrier of ((0). V) by A2, STRUCT_0:def_5;
then  not a in {(0. V)} by VECTSP_4:def_3;
then  a <> 0. V by TARSKI:def_1;
hence  not V is trivial by STRUCT_0:def_18; ::_thesis: verum
end;
now__::_thesis:_(_not_V_is_trivial_implies_W_<>_(0)._V_)
assume  not V is trivial ; ::_thesis: W <> (0). V
then consider a being Vector of V such that
A3: a <> 0. V by STRUCT_0:def_18;
 not a in {(0. V)} by A3, TARSKI:def_1;
then  not a in the carrier of ((0). V) by VECTSP_4:def_3;
hence  W <> (0). V ; ::_thesis: verum
end;
hence  ( V is trivial iff VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) = (0). V ) by A1; ::_thesis: verum
end;

begin

definition
let K be Ring;
let V be LeftMod of K;
let W be strict Subspace of V;
func @ W ->  Element of Submodules V equals :: LMOD_6:def 2
W;
coherence
 W is Element of Submodules V by VECTSP_5:def_3;
end;

:: deftheorem  defines @ LMOD_6:def_2_:_
 for K being Ring
for V being LeftMod of K
for W being strict Subspace of V holds @ W = W;

theorem Th8: :: LMOD_6:8
for K being Ring
for V being LeftMod of K
for W being Subspace of V
for A being Subset of W holds A is Subset of V
proof
let K be Ring; ::_thesis: for V being LeftMod of K
for W being Subspace of V
for A being Subset of W holds A is Subset of V
let V be LeftMod of K; ::_thesis: for W being Subspace of V
for A being Subset of W holds A is Subset of V
let W be Subspace of V; ::_thesis: for A being Subset of W holds A is Subset of V
let A be Subset of W; ::_thesis: A is Subset of V
 the carrier of W c= the carrier of V by VECTSP_4:def_2;
hence  A is Subset of V by XBOOLE_1:1; ::_thesis: verum
end;

definition
let K be Ring;
let V be LeftMod of K;
let W be Subspace of V;
let A be Subset of W;
func @ A ->  Subset of V equals :: LMOD_6:def 3
A;
coherence
 A is Subset of V by Th8;
end;

:: deftheorem  defines @ LMOD_6:def_3_:_
 for K being Ring
for V being LeftMod of K
for W being Subspace of V
for A being Subset of W holds @ A = A;

registration
let K be Ring;
let V be LeftMod of K;
let W be Subspace of V;
let A be non empty Subset of W;
cluster @ A ->  non empty ;
coherence
 not @ A is empty ;
end;

theorem :: LMOD_6:9
for x being set
for K being Ring
for V being LeftMod of K holds
( x in [#] V iff x in V ) by STRUCT_0:def_5;

theorem :: LMOD_6:10
for x being set
for K being Ring
for V being LeftMod of K
for W being Subspace of V holds
( x in @ ([#] W) iff x in W ) by STRUCT_0:def_5;

theorem Th11: :: LMOD_6:11
for K being Ring
for V being LeftMod of K
for A being Subset of V holds A c= [#] (Lin A)
proof
let K be Ring; ::_thesis: for V being LeftMod of K
for A being Subset of V holds A c= [#] (Lin A)
let V be LeftMod of K; ::_thesis: for A being Subset of V holds A c= [#] (Lin A)
let A be Subset of V; ::_thesis: A c= [#] (Lin A)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in [#] (Lin A) )
assume  x in A ; ::_thesis: x in [#] (Lin A)
then  x in Lin A by MOD_3:5;
hence  x in [#] (Lin A) by STRUCT_0:def_5; ::_thesis: verum
end;

theorem Th12: :: LMOD_6:12
for K being Ring
for V being LeftMod of K
for A being Subset of V
for l being Linear_Combination of A st A <> {} & A is linearly-closed holds
Sum l in A
proof
let K be Ring; ::_thesis: for V being LeftMod of K
for A being Subset of V
for l being Linear_Combination of A st A <> {} & A is linearly-closed holds
Sum l in A
let V be LeftMod of K; ::_thesis: for A being Subset of V
for l being Linear_Combination of A st A <> {} & A is linearly-closed holds
Sum l in A
let A be Subset of V; ::_thesis: for l being Linear_Combination of A st A <> {} & A is linearly-closed holds
Sum l in A
let l be Linear_Combination of A; ::_thesis: ( A <> {} & A is linearly-closed implies Sum l in A )
assume A1: ( A <> {} & A is linearly-closed ) ; ::_thesis: Sum l in A
now__::_thesis:_Sum_l_in_A
percases ( 0. K <> 1_ K or 0. K = 1_ K ) ;
suppose 0. K <> 1_ K ; ::_thesis: Sum l in A
hence  Sum l in A by A1, VECTSP_6:14; ::_thesis: verum
end;
suppose 0. K = 1_ K ; ::_thesis: Sum l in A
then  K is trivial by Def1;
then  Sum l = 0. V by Th5;
hence  Sum l in A by A1, VECTSP_4:1; ::_thesis: verum
end;
end;
end;
hence  Sum l in A ; ::_thesis: verum
end;

theorem :: LMOD_6:13
for K being Ring
for V being LeftMod of K
for A being Subset of V st 0. V in A & A is linearly-closed holds
A = [#] (Lin A)
proof
let K be Ring; ::_thesis: for V being LeftMod of K
for A being Subset of V st 0. V in A & A is linearly-closed holds
A = [#] (Lin A)
let V be LeftMod of K; ::_thesis: for A being Subset of V st 0. V in A & A is linearly-closed holds
A = [#] (Lin A)
let A be Subset of V; ::_thesis: ( 0. V in A & A is linearly-closed implies A = [#] (Lin A) )
assume A1: ( 0. V in A & A is linearly-closed ) ; ::_thesis: A = [#] (Lin A)
thus  A c= [#] (Lin A) by Th11; :: according to XBOOLE_0:def_10 ::_thesis: [#] (Lin A) c= A
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [#] (Lin A) or x in A )
assume  x in [#] (Lin A) ; ::_thesis: x in A
then  x in Lin A by STRUCT_0:def_5;
then  ex l being Linear_Combination of A st x = Sum l by MOD_3:4;
hence  x in A by A1, Th12; ::_thesis: verum
end;

begin

definition
let K be Ring;
let V be LeftMod of K;
let a be Vector of V;
func<:a:> ->  strict Subspace of V equals :: LMOD_6:def 4
 Lin {a};
correctness
coherence
Lin {a} is strict Subspace of V;
;
end;

:: deftheorem  defines <: LMOD_6:def_4_:_
 for K being Ring
for V being LeftMod of K
for a being Vector of V holds <:a:> = Lin {a};

begin

definition
let K be Ring;
let M, N be LeftMod of K;
predM c= N means :Def5: :: LMOD_6:def 5
M is Subspace of N;
reflexivity
 for M being LeftMod of K holds M is Subspace of M by VECTSP_4:24;
end;

:: deftheorem Def5 defines c= LMOD_6:def_5_:_
 for K being Ring
for M, N being LeftMod of K holds
( M c= N iff M is Subspace of N );

theorem Th14: :: LMOD_6:14
for x being set
for K being Ring
for M, N being LeftMod of K st M c= N holds
( ( x in M implies x in N ) & ( x is Vector of M implies x is Vector of N ) )
proof
let x be set ; ::_thesis: for K being Ring
for M, N being LeftMod of K st M c= N holds
( ( x in M implies x in N ) & ( x is Vector of M implies x is Vector of N ) )
let K be Ring; ::_thesis: for M, N being LeftMod of K st M c= N holds
( ( x in M implies x in N ) & ( x is Vector of M implies x is Vector of N ) )
let M, N be LeftMod of K; ::_thesis: ( M c= N implies ( ( x in M implies x in N ) & ( x is Vector of M implies x is Vector of N ) ) )
assume A1: M c= N ; ::_thesis: ( ( x in M implies x in N ) & ( x is Vector of M implies x is Vector of N ) )
thus  ( x in M implies x in N ) ::_thesis: ( x is Vector of M implies x is Vector of N )
proof
reconsider M9 = M as Subspace of N by A1, Def5;
assume  x in M ; ::_thesis: x in N
then  x in M9 ;
hence  x in N by VECTSP_4:9; ::_thesis: verum
end;
thus  ( x is Vector of M implies x is Vector of N ) ::_thesis: verum
proof
reconsider M9 = M as Subspace of N by A1, Def5;
assume  x is Vector of M ; ::_thesis: x is Vector of N
then  x is Vector of M9 ;
hence  x is Vector of N by VECTSP_4:10; ::_thesis: verum
end;
end;

theorem :: LMOD_6:15
for K being Ring
for r being Scalar of K
for M, N being LeftMod of K
for m1, m2, m being Vector of M
for n1, n2, n being Vector of N st M c= N holds
( 0. M = 0. N & ( m1 = n1 & m2 = n2 implies m1 + m2 = n1 + n2 ) & ( m = n implies r * m = r * n ) & ( m = n implies - n = - m ) & ( m1 = n1 & m2 = n2 implies m1 - m2 = n1 - n2 ) & 0. N in M & 0. M in N & ( n1 in M & n2 in M implies n1 + n2 in M ) & ( n in M implies r * n in M ) & ( n in M implies - n in M ) & ( n1 in M & n2 in M implies n1 - n2 in M ) )
proof
let K be Ring; ::_thesis: for r being Scalar of K
for M, N being LeftMod of K
for m1, m2, m being Vector of M
for n1, n2, n being Vector of N st M c= N holds
( 0. M = 0. N & ( m1 = n1 & m2 = n2 implies m1 + m2 = n1 + n2 ) & ( m = n implies r * m = r * n ) & ( m = n implies - n = - m ) & ( m1 = n1 & m2 = n2 implies m1 - m2 = n1 - n2 ) & 0. N in M & 0. M in N & ( n1 in M & n2 in M implies n1 + n2 in M ) & ( n in M implies r * n in M ) & ( n in M implies - n in M ) & ( n1 in M & n2 in M implies n1 - n2 in M ) )
let r be Scalar of K; ::_thesis: for M, N being LeftMod of K
for m1, m2, m being Vector of M
for n1, n2, n being Vector of N st M c= N holds
( 0. M = 0. N & ( m1 = n1 & m2 = n2 implies m1 + m2 = n1 + n2 ) & ( m = n implies r * m = r * n ) & ( m = n implies - n = - m ) & ( m1 = n1 & m2 = n2 implies m1 - m2 = n1 - n2 ) & 0. N in M & 0. M in N & ( n1 in M & n2 in M implies n1 + n2 in M ) & ( n in M implies r * n in M ) & ( n in M implies - n in M ) & ( n1 in M & n2 in M implies n1 - n2 in M ) )
let M, N be LeftMod of K; ::_thesis: for m1, m2, m being Vector of M
for n1, n2, n being Vector of N st M c= N holds
( 0. M = 0. N & ( m1 = n1 & m2 = n2 implies m1 + m2 = n1 + n2 ) & ( m = n implies r * m = r * n ) & ( m = n implies - n = - m ) & ( m1 = n1 & m2 = n2 implies m1 - m2 = n1 - n2 ) & 0. N in M & 0. M in N & ( n1 in M & n2 in M implies n1 + n2 in M ) & ( n in M implies r * n in M ) & ( n in M implies - n in M ) & ( n1 in M & n2 in M implies n1 - n2 in M ) )
let m1, m2, m be Vector of M; ::_thesis: for n1, n2, n being Vector of N st M c= N holds
( 0. M = 0. N & ( m1 = n1 & m2 = n2 implies m1 + m2 = n1 + n2 ) & ( m = n implies r * m = r * n ) & ( m = n implies - n = - m ) & ( m1 = n1 & m2 = n2 implies m1 - m2 = n1 - n2 ) & 0. N in M & 0. M in N & ( n1 in M & n2 in M implies n1 + n2 in M ) & ( n in M implies r * n in M ) & ( n in M implies - n in M ) & ( n1 in M & n2 in M implies n1 - n2 in M ) )
let n1, n2, n be Vector of N; ::_thesis: ( M c= N implies ( 0. M = 0. N & ( m1 = n1 & m2 = n2 implies m1 + m2 = n1 + n2 ) & ( m = n implies r * m = r * n ) & ( m = n implies - n = - m ) & ( m1 = n1 & m2 = n2 implies m1 - m2 = n1 - n2 ) & 0. N in M & 0. M in N & ( n1 in M & n2 in M implies n1 + n2 in M ) & ( n in M implies r * n in M ) & ( n in M implies - n in M ) & ( n1 in M & n2 in M implies n1 - n2 in M ) ) )
assume A1: M c= N ; ::_thesis: ( 0. M = 0. N & ( m1 = n1 & m2 = n2 implies m1 + m2 = n1 + n2 ) & ( m = n implies r * m = r * n ) & ( m = n implies - n = - m ) & ( m1 = n1 & m2 = n2 implies m1 - m2 = n1 - n2 ) & 0. N in M & 0. M in N & ( n1 in M & n2 in M implies n1 + n2 in M ) & ( n in M implies r * n in M ) & ( n in M implies - n in M ) & ( n1 in M & n2 in M implies n1 - n2 in M ) )
thus  0. M = 0. N ::_thesis: ( ( m1 = n1 & m2 = n2 implies m1 + m2 = n1 + n2 ) & ( m = n implies r * m = r * n ) & ( m = n implies - n = - m ) & ( m1 = n1 & m2 = n2 implies m1 - m2 = n1 - n2 ) & 0. N in M & 0. M in N & ( n1 in M & n2 in M implies n1 + n2 in M ) & ( n in M implies r * n in M ) & ( n in M implies - n in M ) & ( n1 in M & n2 in M implies n1 - n2 in M ) )
proof
reconsider M9 = M as Subspace of N by A1, Def5;
 0. M9 = 0. N by VECTSP_4:11;
hence  0. M = 0. N ; ::_thesis: verum
end;
thus  ( m1 = n1 & m2 = n2 implies m1 + m2 = n1 + n2 ) ::_thesis: ( ( m = n implies r * m = r * n ) & ( m = n implies - n = - m ) & ( m1 = n1 & m2 = n2 implies m1 - m2 = n1 - n2 ) & 0. N in M & 0. M in N & ( n1 in M & n2 in M implies n1 + n2 in M ) & ( n in M implies r * n in M ) & ( n in M implies - n in M ) & ( n1 in M & n2 in M implies n1 - n2 in M ) )
proof
reconsider M9 = M as Subspace of N by A1, Def5;
assume that
A2: m1 = n1 and
A3: m2 = n2 ; ::_thesis: m1 + m2 = n1 + n2
reconsider m19 = m1 as Vector of M9 ;
 m19 = n1 by A2;
hence  m1 + m2 = n1 + n2 by A3, VECTSP_4:13; ::_thesis: verum
end;
thus  ( m = n implies r * m = r * n ) ::_thesis: ( ( m = n implies - n = - m ) & ( m1 = n1 & m2 = n2 implies m1 - m2 = n1 - n2 ) & 0. N in M & 0. M in N & ( n1 in M & n2 in M implies n1 + n2 in M ) & ( n in M implies r * n in M ) & ( n in M implies - n in M ) & ( n1 in M & n2 in M implies n1 - n2 in M ) )
proof
reconsider M9 = M as Subspace of N by A1, Def5;
reconsider m9 = m as Vector of M9 ;
assume  m = n ; ::_thesis: r * m = r * n
then  m9 = n ;
hence  r * m = r * n by VECTSP_4:14; ::_thesis: verum
end;
thus  ( m = n implies - n = - m ) ::_thesis: ( ( m1 = n1 & m2 = n2 implies m1 - m2 = n1 - n2 ) & 0. N in M & 0. M in N & ( n1 in M & n2 in M implies n1 + n2 in M ) & ( n in M implies r * n in M ) & ( n in M implies - n in M ) & ( n1 in M & n2 in M implies n1 - n2 in M ) )
proof
reconsider M9 = M as Subspace of N by A1, Def5;
reconsider m9 = m as Vector of M9 ;
assume  m = n ; ::_thesis: - n = - m
then  m9 = n ;
hence  - n = - m by VECTSP_4:15; ::_thesis: verum
end;
thus  ( m1 = n1 & m2 = n2 implies m1 - m2 = n1 - n2 ) ::_thesis: ( 0. N in M & 0. M in N & ( n1 in M & n2 in M implies n1 + n2 in M ) & ( n in M implies r * n in M ) & ( n in M implies - n in M ) & ( n1 in M & n2 in M implies n1 - n2 in M ) )
proof
reconsider M9 = M as Subspace of N by A1, Def5;
assume that
A4: m1 = n1 and
A5: m2 = n2 ; ::_thesis: m1 - m2 = n1 - n2
reconsider m19 = m1 as Vector of M9 ;
 m19 = n1 by A4;
hence  m1 - m2 = n1 - n2 by A5, VECTSP_4:16; ::_thesis: verum
end;
thus  0. N in M ::_thesis: ( 0. M in N & ( n1 in M & n2 in M implies n1 + n2 in M ) & ( n in M implies r * n in M ) & ( n in M implies - n in M ) & ( n1 in M & n2 in M implies n1 - n2 in M ) )
proof
reconsider M9 = M as Subspace of N by A1, Def5;
 0. N in M9 by VECTSP_4:17;
hence  0. N in M ; ::_thesis: verum
end;
thus  0. M in N ::_thesis: ( ( n1 in M & n2 in M implies n1 + n2 in M ) & ( n in M implies r * n in M ) & ( n in M implies - n in M ) & ( n1 in M & n2 in M implies n1 - n2 in M ) )
proof
reconsider M9 = M as Subspace of N by A1, Def5;
 0. M9 in N by VECTSP_4:19;
hence  0. M in N ; ::_thesis: verum
end;
thus  ( n1 in M & n2 in M implies n1 + n2 in M ) ::_thesis: ( ( n in M implies r * n in M ) & ( n in M implies - n in M ) & ( n1 in M & n2 in M implies n1 - n2 in M ) )
proof
reconsider M9 = M as Subspace of N by A1, Def5;
assume that
A6: n1 in M and
A7: n2 in M ; ::_thesis: n1 + n2 in M
 n1 in M9 by A6;
hence  n1 + n2 in M by A7, VECTSP_4:20; ::_thesis: verum
end;
thus  ( n in M implies r * n in M ) ::_thesis: ( ( n in M implies - n in M ) & ( n1 in M & n2 in M implies n1 - n2 in M ) )
proof
reconsider M9 = M as Subspace of N by A1, Def5;
assume  n in M ; ::_thesis: r * n in M
then  n in M9 ;
hence  r * n in M by VECTSP_4:21; ::_thesis: verum
end;
thus  ( n in M implies - n in M ) ::_thesis: ( n1 in M & n2 in M implies n1 - n2 in M )
proof
reconsider M9 = M as Subspace of N by A1, Def5;
assume  n in M ; ::_thesis: - n in M
then  n in M9 ;
hence  - n in M by VECTSP_4:22; ::_thesis: verum
end;
thus  ( n1 in M & n2 in M implies n1 - n2 in M ) ::_thesis: verum
proof
reconsider M9 = M as Subspace of N by A1, Def5;
assume that
A8: n1 in M and
A9: n2 in M ; ::_thesis: n1 - n2 in M
 n1 in M9 by A8;
hence  n1 - n2 in M by A9, VECTSP_4:23; ::_thesis: verum
end;
end;

theorem :: LMOD_6:16
for K being Ring
for M1, N, M2 being LeftMod of K st M1 c= N & M2 c= N holds
( 0. M1 = 0. M2 & 0. M1 in M2 & ( the carrier of M1 c= the carrier of M2 implies M1 c= M2 ) & ( ( for n being Vector of N st n in M1 holds
n in M2 ) implies M1 c= M2 ) & ( the carrier of M1 = the carrier of M2 & M1 is strict & M2 is strict implies M1 = M2 ) & (0). M1 c= M2 )
proof
let K be Ring; ::_thesis: for M1, N, M2 being LeftMod of K st M1 c= N & M2 c= N holds
( 0. M1 = 0. M2 & 0. M1 in M2 & ( the carrier of M1 c= the carrier of M2 implies M1 c= M2 ) & ( ( for n being Vector of N st n in M1 holds
n in M2 ) implies M1 c= M2 ) & ( the carrier of M1 = the carrier of M2 & M1 is strict & M2 is strict implies M1 = M2 ) & (0). M1 c= M2 )
let M1, N, M2 be LeftMod of K; ::_thesis: ( M1 c= N & M2 c= N implies ( 0. M1 = 0. M2 & 0. M1 in M2 & ( the carrier of M1 c= the carrier of M2 implies M1 c= M2 ) & ( ( for n being Vector of N st n in M1 holds
n in M2 ) implies M1 c= M2 ) & ( the carrier of M1 = the carrier of M2 & M1 is strict & M2 is strict implies M1 = M2 ) & (0). M1 c= M2 ) )
assume that
A1: M1 c= N and
A2: M2 c= N ; ::_thesis: ( 0. M1 = 0. M2 & 0. M1 in M2 & ( the carrier of M1 c= the carrier of M2 implies M1 c= M2 ) & ( ( for n being Vector of N st n in M1 holds
n in M2 ) implies M1 c= M2 ) & ( the carrier of M1 = the carrier of M2 & M1 is strict & M2 is strict implies M1 = M2 ) & (0). M1 c= M2 )
thus  0. M1 = 0. M2 ::_thesis: ( 0. M1 in M2 & ( the carrier of M1 c= the carrier of M2 implies M1 c= M2 ) & ( ( for n being Vector of N st n in M1 holds
n in M2 ) implies M1 c= M2 ) & ( the carrier of M1 = the carrier of M2 & M1 is strict & M2 is strict implies M1 = M2 ) & (0). M1 c= M2 )
proof
reconsider M19 = M1, M29 = M2 as Subspace of N by A1, A2, Def5;
 0. M19 = 0. M29 by VECTSP_4:12;
hence  0. M1 = 0. M2 ; ::_thesis: verum
end;
thus  0. M1 in M2 ::_thesis: ( ( the carrier of M1 c= the carrier of M2 implies M1 c= M2 ) & ( ( for n being Vector of N st n in M1 holds
n in M2 ) implies M1 c= M2 ) & ( the carrier of M1 = the carrier of M2 & M1 is strict & M2 is strict implies M1 = M2 ) & (0). M1 c= M2 )
proof
reconsider M19 = M1, M29 = M2 as Subspace of N by A1, A2, Def5;
 0. M19 in M29 by VECTSP_4:18;
hence  0. M1 in M2 ; ::_thesis: verum
end;
thus  ( the carrier of M1 c= the carrier of M2 implies M1 c= M2 ) ::_thesis: ( ( ( for n being Vector of N st n in M1 holds
n in M2 ) implies M1 c= M2 ) & ( the carrier of M1 = the carrier of M2 & M1 is strict & M2 is strict implies M1 = M2 ) & (0). M1 c= M2 )
proof
reconsider M19 = M1, M29 = M2 as Subspace of N by A1, A2, Def5;
assume  the carrier of M1 c= the carrier of M2 ; ::_thesis: M1 c= M2
then  M19 is Subspace of M29 by VECTSP_4:27;
hence  M1 c= M2 by Def5; ::_thesis: verum
end;
thus  ( ( for n being Vector of N st n in M1 holds
n in M2 ) implies M1 c= M2 ) ::_thesis: ( ( the carrier of M1 = the carrier of M2 & M1 is strict & M2 is strict implies M1 = M2 ) & (0). M1 c= M2 )
proof
reconsider M19 = M1, M29 = M2 as Subspace of N by A1, A2, Def5;
assume  for n being Vector of N st n in M1 holds
n in M2 ; ::_thesis: M1 c= M2
then  M19 is Subspace of M29 by VECTSP_4:28;
hence  M1 c= M2 by Def5; ::_thesis: verum
end;
thus  ( the carrier of M1 = the carrier of M2 & M1 is strict & M2 is strict implies M1 = M2 ) ::_thesis: (0). M1 c= M2
proof
assume that
A3: the carrier of M1 = the carrier of M2 and
A4: M1 is strict and
A5: M2 is strict ; ::_thesis: M1 = M2
reconsider M29 = M2 as strict Subspace of N by A2, A5, Def5;
reconsider M19 = M1 as strict Subspace of N by A1, A4, Def5;
 M19 = M29 by A3, VECTSP_4:29;
hence  M1 = M2 ; ::_thesis: verum
end;
thus  (0). M1 c= M2 ::_thesis: verum
proof
reconsider M19 = M1, M29 = M2 as Subspace of N by A1, A2, Def5;
 (0). M19 is Subspace of M29 by VECTSP_4:40;
hence  (0). M1 c= M2 by Def5; ::_thesis: verum
end;
end;

theorem :: LMOD_6:17
for K being Ring
for V, M being strict LeftMod of K st V c= M & M c= V holds
V = M
proof
let K be Ring; ::_thesis: for V, M being strict LeftMod of K st V c= M & M c= V holds
V = M
let V, M be strict LeftMod of K; ::_thesis: ( V c= M & M c= V implies V = M )
assume  ( V c= M & M c= V ) ; ::_thesis: V = M
then  ( V is Subspace of M & M is Subspace of V ) by Def5;
hence  V = M by VECTSP_4:25; ::_thesis: verum
end;

theorem :: LMOD_6:18
for K being Ring
for V, M, N being LeftMod of K st V c= M & M c= N holds
V c= N
proof
let K be Ring; ::_thesis: for V, M, N being LeftMod of K st V c= M & M c= N holds
V c= N
let V, M, N be LeftMod of K; ::_thesis: ( V c= M & M c= N implies V c= N )
assume  ( V c= M & M c= N ) ; ::_thesis: V c= N
then  ( V is Subspace of M & M is Subspace of N ) by Def5;
then  V is Subspace of N by VECTSP_4:26;
hence  V c= N by Def5; ::_thesis: verum
end;

theorem :: LMOD_6:19
for K being Ring
for M, N being LeftMod of K st M c= N holds
(0). M c= N
proof
let K be Ring; ::_thesis: for M, N being LeftMod of K st M c= N holds
(0). M c= N
let M, N be LeftMod of K; ::_thesis: ( M c= N implies (0). M c= N )
assume  M c= N ; ::_thesis: (0). M c= N
then reconsider M9 = M as Subspace of N by Def5;
 (0). M9 is Subspace of N by VECTSP_4:38;
hence  (0). M c= N by Def5; ::_thesis: verum
end;

theorem :: LMOD_6:20
for K being Ring
for M, N being LeftMod of K st M c= N holds
(0). N c= M
proof
let K be Ring; ::_thesis: for M, N being LeftMod of K st M c= N holds
(0). N c= M
let M, N be LeftMod of K; ::_thesis: ( M c= N implies (0). N c= M )
assume  M c= N ; ::_thesis: (0). N c= M
then reconsider M9 = M as Subspace of N by Def5;
 (0). N is Subspace of M9 by VECTSP_4:39;
hence  (0). N c= M by Def5; ::_thesis: verum
end;

theorem :: LMOD_6:21
for K being Ring
for M, N being LeftMod of K st M c= N holds
M c= (Omega). N
proof
let K be Ring; ::_thesis: for M, N being LeftMod of K st M c= N holds
M c= (Omega). N
let M, N be LeftMod of K; ::_thesis: ( M c= N implies M c= (Omega). N )
assume  M c= N ; ::_thesis: M c= (Omega). N
then A1: M is Subspace of N by Def5;
 N is Subspace of (Omega). N by Th4;
then  M is Subspace of (Omega). N by A1, VECTSP_4:26;
hence  M c= (Omega). N by Def5; ::_thesis: verum
end;

theorem :: LMOD_6:22
for K being Ring
for V being LeftMod of K
for W1, W2 being Subspace of V holds
( W1 c= W1 + W2 & W2 c= W1 + W2 )
proof
let K be Ring; ::_thesis: for V being LeftMod of K
for W1, W2 being Subspace of V holds
( W1 c= W1 + W2 & W2 c= W1 + W2 )
let V be LeftMod of K; ::_thesis: for W1, W2 being Subspace of V holds
( W1 c= W1 + W2 & W2 c= W1 + W2 )
let W1, W2 be Subspace of V; ::_thesis: ( W1 c= W1 + W2 & W2 c= W1 + W2 )
 ( W1 is Subspace of W1 + W2 & W2 is Subspace of W1 + W2 ) by VECTSP_5:7;
hence  ( W1 c= W1 + W2 & W2 c= W1 + W2 ) by Def5; ::_thesis: verum
end;

theorem :: LMOD_6:23
for K being Ring
for V being LeftMod of K
for W1, W2 being Subspace of V holds
( W1 /\ W2 c= W1 & W1 /\ W2 c= W2 )
proof
let K be Ring; ::_thesis: for V being LeftMod of K
for W1, W2 being Subspace of V holds
( W1 /\ W2 c= W1 & W1 /\ W2 c= W2 )
let V be LeftMod of K; ::_thesis: for W1, W2 being Subspace of V holds
( W1 /\ W2 c= W1 & W1 /\ W2 c= W2 )
let W1, W2 be Subspace of V; ::_thesis: ( W1 /\ W2 c= W1 & W1 /\ W2 c= W2 )
 ( W1 /\ W2 is Subspace of W1 & W1 /\ W2 is Subspace of W2 ) by VECTSP_5:15;
hence  ( W1 /\ W2 c= W1 & W1 /\ W2 c= W2 ) by Def5; ::_thesis: verum
end;

theorem :: LMOD_6:24
for K being Ring
for V being LeftMod of K
for W1, W2, W3 being Subspace of V st W1 c= W2 holds
W1 /\ W3 c= W2 /\ W3
proof
let K be Ring; ::_thesis: for V being LeftMod of K
for W1, W2, W3 being Subspace of V st W1 c= W2 holds
W1 /\ W3 c= W2 /\ W3
let V be LeftMod of K; ::_thesis: for W1, W2, W3 being Subspace of V st W1 c= W2 holds
W1 /\ W3 c= W2 /\ W3
let W1, W2, W3 be Subspace of V; ::_thesis: ( W1 c= W2 implies W1 /\ W3 c= W2 /\ W3 )
 ( W1 is Subspace of W2 implies W1 /\ W3 is Subspace of W2 /\ W3 ) by VECTSP_5:17;
hence  ( W1 c= W2 implies W1 /\ W3 c= W2 /\ W3 ) by Def5; ::_thesis: verum
end;

theorem :: LMOD_6:25
for K being Ring
for V being LeftMod of K
for W1, W3, W2 being Subspace of V st W1 c= W3 holds
W1 /\ W2 c= W3
proof
let K be Ring; ::_thesis: for V being LeftMod of K
for W1, W3, W2 being Subspace of V st W1 c= W3 holds
W1 /\ W2 c= W3
let V be LeftMod of K; ::_thesis: for W1, W3, W2 being Subspace of V st W1 c= W3 holds
W1 /\ W2 c= W3
let W1, W3, W2 be Subspace of V; ::_thesis: ( W1 c= W3 implies W1 /\ W2 c= W3 )
 ( W1 is Subspace of W3 implies W1 /\ W2 is Subspace of W3 ) by VECTSP_5:18;
hence  ( W1 c= W3 implies W1 /\ W2 c= W3 ) by Def5; ::_thesis: verum
end;

theorem :: LMOD_6:26
for K being Ring
for V being LeftMod of K
for W1, W2, W3 being Subspace of V st W1 c= W2 & W1 c= W3 holds
W1 c= W2 /\ W3
proof
let K be Ring; ::_thesis: for V being LeftMod of K
for W1, W2, W3 being Subspace of V st W1 c= W2 & W1 c= W3 holds
W1 c= W2 /\ W3
let V be LeftMod of K; ::_thesis: for W1, W2, W3 being Subspace of V st W1 c= W2 & W1 c= W3 holds
W1 c= W2 /\ W3
let W1, W2, W3 be Subspace of V; ::_thesis: ( W1 c= W2 & W1 c= W3 implies W1 c= W2 /\ W3 )
 ( W1 is Subspace of W2 & W1 is Subspace of W3 implies W1 is Subspace of W2 /\ W3 ) by VECTSP_5:19;
hence  ( W1 c= W2 & W1 c= W3 implies W1 c= W2 /\ W3 ) by Def5; ::_thesis: verum
end;

theorem :: LMOD_6:27
for K being Ring
for V being LeftMod of K
for W1, W2 being Subspace of V holds W1 /\ W2 c= W1 + W2
proof
let K be Ring; ::_thesis: for V being LeftMod of K
for W1, W2 being Subspace of V holds W1 /\ W2 c= W1 + W2
let V be LeftMod of K; ::_thesis: for W1, W2 being Subspace of V holds W1 /\ W2 c= W1 + W2
let W1, W2 be Subspace of V; ::_thesis: W1 /\ W2 c= W1 + W2
 W1 /\ W2 is Subspace of W1 + W2 by VECTSP_5:23;
hence  W1 /\ W2 c= W1 + W2 by Def5; ::_thesis: verum
end;

theorem :: LMOD_6:28
for K being Ring
for V being LeftMod of K
for W1, W2, W3 being Subspace of V holds (W1 /\ W2) + (W2 /\ W3) c= W2 /\ (W1 + W3)
proof
let K be Ring; ::_thesis: for V being LeftMod of K
for W1, W2, W3 being Subspace of V holds (W1 /\ W2) + (W2 /\ W3) c= W2 /\ (W1 + W3)
let V be LeftMod of K; ::_thesis: for W1, W2, W3 being Subspace of V holds (W1 /\ W2) + (W2 /\ W3) c= W2 /\ (W1 + W3)
let W1, W2, W3 be Subspace of V; ::_thesis: (W1 /\ W2) + (W2 /\ W3) c= W2 /\ (W1 + W3)
 (W1 /\ W2) + (W2 /\ W3) is Subspace of W2 /\ (W1 + W3) by VECTSP_5:26;
hence  (W1 /\ W2) + (W2 /\ W3) c= W2 /\ (W1 + W3) by Def5; ::_thesis: verum
end;

theorem :: LMOD_6:29
for K being Ring
for V being LeftMod of K
for W1, W2, W3 being Subspace of V st W1 c= W2 holds
W2 /\ (W1 + W3) = (W1 /\ W2) + (W2 /\ W3)
proof
let K be Ring; ::_thesis: for V being LeftMod of K
for W1, W2, W3 being Subspace of V st W1 c= W2 holds
W2 /\ (W1 + W3) = (W1 /\ W2) + (W2 /\ W3)
let V be LeftMod of K; ::_thesis: for W1, W2, W3 being Subspace of V st W1 c= W2 holds
W2 /\ (W1 + W3) = (W1 /\ W2) + (W2 /\ W3)
let W1, W2, W3 be Subspace of V; ::_thesis: ( W1 c= W2 implies W2 /\ (W1 + W3) = (W1 /\ W2) + (W2 /\ W3) )
 ( W1 is Subspace of W2 implies W2 /\ (W1 + W3) = (W1 /\ W2) + (W2 /\ W3) ) by VECTSP_5:27;
hence  ( W1 c= W2 implies W2 /\ (W1 + W3) = (W1 /\ W2) + (W2 /\ W3) ) by Def5; ::_thesis: verum
end;

theorem :: LMOD_6:30
for K being Ring
for V being LeftMod of K
for W2, W1, W3 being Subspace of V holds W2 + (W1 /\ W3) c= (W1 + W2) /\ (W2 + W3)
proof
let K be Ring; ::_thesis: for V being LeftMod of K
for W2, W1, W3 being Subspace of V holds W2 + (W1 /\ W3) c= (W1 + W2) /\ (W2 + W3)
let V be LeftMod of K; ::_thesis: for W2, W1, W3 being Subspace of V holds W2 + (W1 /\ W3) c= (W1 + W2) /\ (W2 + W3)
let W2, W1, W3 be Subspace of V; ::_thesis: W2 + (W1 /\ W3) c= (W1 + W2) /\ (W2 + W3)
 W2 + (W1 /\ W3) is Subspace of (W1 + W2) /\ (W2 + W3) by VECTSP_5:28;
hence  W2 + (W1 /\ W3) c= (W1 + W2) /\ (W2 + W3) by Def5; ::_thesis: verum
end;

theorem :: LMOD_6:31
for K being Ring
for V being LeftMod of K
for W1, W2, W3 being Subspace of V st W1 c= W2 holds
W2 + (W1 /\ W3) = (W1 + W2) /\ (W2 + W3)
proof
let K be Ring; ::_thesis: for V being LeftMod of K
for W1, W2, W3 being Subspace of V st W1 c= W2 holds
W2 + (W1 /\ W3) = (W1 + W2) /\ (W2 + W3)
let V be LeftMod of K; ::_thesis: for W1, W2, W3 being Subspace of V st W1 c= W2 holds
W2 + (W1 /\ W3) = (W1 + W2) /\ (W2 + W3)
let W1, W2, W3 be Subspace of V; ::_thesis: ( W1 c= W2 implies W2 + (W1 /\ W3) = (W1 + W2) /\ (W2 + W3) )
 ( W1 is Subspace of W2 implies W2 + (W1 /\ W3) = (W1 + W2) /\ (W2 + W3) ) by VECTSP_5:29;
hence  ( W1 c= W2 implies W2 + (W1 /\ W3) = (W1 + W2) /\ (W2 + W3) ) by Def5; ::_thesis: verum
end;

theorem :: LMOD_6:32
for K being Ring
for V being LeftMod of K
for W1, W2, W3 being Subspace of V st W1 c= W2 holds
W1 c= W2 + W3
proof
let K be Ring; ::_thesis: for V being LeftMod of K
for W1, W2, W3 being Subspace of V st W1 c= W2 holds
W1 c= W2 + W3
let V be LeftMod of K; ::_thesis: for W1, W2, W3 being Subspace of V st W1 c= W2 holds
W1 c= W2 + W3
let W1, W2, W3 be Subspace of V; ::_thesis: ( W1 c= W2 implies W1 c= W2 + W3 )
 ( W1 is Subspace of W2 implies W1 is Subspace of W2 + W3 ) by VECTSP_5:33;
hence  ( W1 c= W2 implies W1 c= W2 + W3 ) by Def5; ::_thesis: verum
end;

theorem :: LMOD_6:33
for K being Ring
for V being LeftMod of K
for W1, W3, W2 being Subspace of V st W1 c= W3 & W2 c= W3 holds
W1 + W2 c= W3
proof
let K be Ring; ::_thesis: for V being LeftMod of K
for W1, W3, W2 being Subspace of V st W1 c= W3 & W2 c= W3 holds
W1 + W2 c= W3
let V be LeftMod of K; ::_thesis: for W1, W3, W2 being Subspace of V st W1 c= W3 & W2 c= W3 holds
W1 + W2 c= W3
let W1, W3, W2 be Subspace of V; ::_thesis: ( W1 c= W3 & W2 c= W3 implies W1 + W2 c= W3 )
 ( W1 is Subspace of W3 & W2 is Subspace of W3 implies W1 + W2 is Subspace of W3 ) by VECTSP_5:34;
hence  ( W1 c= W3 & W2 c= W3 implies W1 + W2 c= W3 ) by Def5; ::_thesis: verum
end;

theorem :: LMOD_6:34
for K being Ring
for V being LeftMod of K
for A, B being Subset of V st A c= B holds
Lin A c= Lin B
proof
let K be Ring; ::_thesis: for V being LeftMod of K
for A, B being Subset of V st A c= B holds
Lin A c= Lin B
let V be LeftMod of K; ::_thesis: for A, B being Subset of V st A c= B holds
Lin A c= Lin B
let A, B be Subset of V; ::_thesis: ( A c= B implies Lin A c= Lin B )
assume  A c= B ; ::_thesis: Lin A c= Lin B
then  Lin A is Subspace of Lin B by MOD_3:10;
hence  Lin A c= Lin B by Def5; ::_thesis: verum
end;

theorem :: LMOD_6:35
for K being Ring
for V being LeftMod of K
for A, B being Subset of V holds Lin (A /\ B) c= (Lin A) /\ (Lin B)
proof
let K be Ring; ::_thesis: for V being LeftMod of K
for A, B being Subset of V holds Lin (A /\ B) c= (Lin A) /\ (Lin B)
let V be LeftMod of K; ::_thesis: for A, B being Subset of V holds Lin (A /\ B) c= (Lin A) /\ (Lin B)
let A, B be Subset of V; ::_thesis: Lin (A /\ B) c= (Lin A) /\ (Lin B)
 Lin (A /\ B) is Subspace of (Lin A) /\ (Lin B) by MOD_3:13;
hence  Lin (A /\ B) c= (Lin A) /\ (Lin B) by Def5; ::_thesis: verum
end;

theorem Th36: :: LMOD_6:36
for K being Ring
for M1, M2 being LeftMod of K st M1 c= M2 holds
[#] M1 c= [#] M2
proof
let K be Ring; ::_thesis: for M1, M2 being LeftMod of K st M1 c= M2 holds
[#] M1 c= [#] M2
let M1, M2 be LeftMod of K; ::_thesis: ( M1 c= M2 implies [#] M1 c= [#] M2 )
assume A1: M1 c= M2 ; ::_thesis: [#] M1 c= [#] M2
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [#] M1 or x in [#] M2 )
assume  x in [#] M1 ; ::_thesis: x in [#] M2
then  x in M1 by STRUCT_0:def_5;
then  x in M2 by A1, Th14;
hence  x in [#] M2 by STRUCT_0:def_5; ::_thesis: verum
end;

theorem Th37: :: LMOD_6:37
for K being Ring
for V being LeftMod of K
for W1, W2 being Subspace of V holds
( W1 c= W2 iff for a being Vector of V st a in W1 holds
a in W2 )
proof
let K be Ring; ::_thesis: for V being LeftMod of K
for W1, W2 being Subspace of V holds
( W1 c= W2 iff for a being Vector of V st a in W1 holds
a in W2 )
let V be LeftMod of K; ::_thesis: for W1, W2 being Subspace of V holds
( W1 c= W2 iff for a being Vector of V st a in W1 holds
a in W2 )
let W1, W2 be Subspace of V; ::_thesis: ( W1 c= W2 iff for a being Vector of V st a in W1 holds
a in W2 )
 ( W1 c= W2 iff W1 is Subspace of W2 ) by Def5;
hence  ( W1 c= W2 iff for a being Vector of V st a in W1 holds
a in W2 ) by VECTSP_4:8, VECTSP_4:28; ::_thesis: verum
end;

theorem Th38: :: LMOD_6:38
for K being Ring
for V being LeftMod of K
for W1, W2 being Subspace of V holds
( W1 c= W2 iff [#] W1 c= [#] W2 )
proof
let K be Ring; ::_thesis: for V being LeftMod of K
for W1, W2 being Subspace of V holds
( W1 c= W2 iff [#] W1 c= [#] W2 )
let V be LeftMod of K; ::_thesis: for W1, W2 being Subspace of V holds
( W1 c= W2 iff [#] W1 c= [#] W2 )
let W1, W2 be Subspace of V; ::_thesis: ( W1 c= W2 iff [#] W1 c= [#] W2 )
thus  ( W1 c= W2 implies [#] W1 c= [#] W2 ) by Th36; ::_thesis: ( [#] W1 c= [#] W2 implies W1 c= W2 )
assume A1: [#] W1 c= [#] W2 ; ::_thesis: W1 c= W2
now__::_thesis:_for_a_being_Vector_of_V_st_a_in_W1_holds_
a_in_W2
let a be Vector of V; ::_thesis: ( a in W1 implies a in W2 )
assume  a in W1 ; ::_thesis: a in W2
then  a in [#] W1 by STRUCT_0:def_5;
hence  a in W2 by A1, STRUCT_0:def_5; ::_thesis: verum
end;
hence  W1 c= W2 by Th37; ::_thesis: verum
end;

theorem :: LMOD_6:39
for K being Ring
for V being LeftMod of K
for W1, W2 being Subspace of V holds
( W1 c= W2 iff @ ([#] W1) c= @ ([#] W2) ) by Th38;

theorem :: LMOD_6:40
for K being Ring
for V being LeftMod of K
for W, W1, W2 being Subspace of V holds
( (0). W c= V & (0). V c= W & (0). W1 c= W2 )
proof
let K be Ring; ::_thesis: for V being LeftMod of K
for W, W1, W2 being Subspace of V holds
( (0). W c= V & (0). V c= W & (0). W1 c= W2 )
let V be LeftMod of K; ::_thesis: for W, W1, W2 being Subspace of V holds
( (0). W c= V & (0). V c= W & (0). W1 c= W2 )
let W, W1, W2 be Subspace of V; ::_thesis: ( (0). W c= V & (0). V c= W & (0). W1 c= W2 )
 (0). W is Subspace of V by VECTSP_4:38;
hence  (0). W c= V by Def5; ::_thesis: ( (0). V c= W & (0). W1 c= W2 )
 (0). V is Subspace of W by VECTSP_4:39;
hence  (0). V c= W by Def5; ::_thesis: (0). W1 c= W2
 (0). W1 is Subspace of W2 by VECTSP_4:40;
hence  (0). W1 c= W2 by Def5; ::_thesis: verum
end;