:: Submodule of free $\mathbb Z$-module
:: by Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama
::
:: Copyright (c) 2013-2019 Association of Mizar Users

Lem1: for i being Integer holds i in the carrier of INT.Ring
proof end;

theorem :: ZMODUL04:1
for R being Ring
for V being LeftMod of R
for W1, W2 being Subspace of V
for WW1, WW2 being Subspace of W1 + W2 st WW1 = W1 & WW2 = W2 holds
W1 + W2 = WW1 + WW2
proof end;

theorem :: ZMODUL04:2
for R being Ring
for V being LeftMod of R
for W1, W2 being Subspace of V
for WW1, WW2 being Subspace of W1 + W2 st WW1 = W1 & WW2 = W2 holds
W1 /\ W2 = WW1 /\ WW2
proof end;

Lm19: for A, B being set st ( for z being object st z in A holds
ex x, y being object st z = [x,y] ) & ( for z being object st z in B holds
ex x, y being object st z = [x,y] ) & ( for x, y being object holds
( [x,y] in A iff [x,y] in B ) ) holds
A = B

proof end;

registration
let V be Z_Module;
cluster [: the carrier of V,():] -> non empty ;
coherence
not [: the carrier of V,():] is empty
proof end;
end;

definition
let V be Z_Module;
assume AS: V is Mult-cancelable ;
func EQRZM V -> Equivalence_Relation of [: the carrier of V,():] means :defEQRZM: :: ZMODUL04:def 1
for S, T being object holds
( [S,T] in it iff ( S in [: the carrier of V,():] & T in [: the carrier of V,():] & ex z1, z2 being Element of V ex i1, i2 being Element of INT.Ring st
( S = [z1,i1] & T = [z2,i2] & i1 <> 0 & i2 <> 0 & i2 * z1 = i1 * z2 ) ) );
existence
ex b1 being Equivalence_Relation of [: the carrier of V,():] st
for S, T being object holds
( [S,T] in b1 iff ( S in [: the carrier of V,():] & T in [: the carrier of V,():] & ex z1, z2 being Element of V ex i1, i2 being Element of INT.Ring st
( S = [z1,i1] & T = [z2,i2] & i1 <> 0 & i2 <> 0 & i2 * z1 = i1 * z2 ) ) )
proof end;
uniqueness
for b1, b2 being Equivalence_Relation of [: the carrier of V,():] st ( for S, T being object holds
( [S,T] in b1 iff ( S in [: the carrier of V,():] & T in [: the carrier of V,():] & ex z1, z2 being Element of V ex i1, i2 being Element of INT.Ring st
( S = [z1,i1] & T = [z2,i2] & i1 <> 0 & i2 <> 0 & i2 * z1 = i1 * z2 ) ) ) ) & ( for S, T being object holds
( [S,T] in b2 iff ( S in [: the carrier of V,():] & T in [: the carrier of V,():] & ex z1, z2 being Element of V ex i1, i2 being Element of INT.Ring st
( S = [z1,i1] & T = [z2,i2] & i1 <> 0 & i2 <> 0 & i2 * z1 = i1 * z2 ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem defEQRZM defines EQRZM ZMODUL04:def 1 :
for V being Z_Module st V is Mult-cancelable holds
for b2 being Equivalence_Relation of [: the carrier of V,():] holds
( b2 = EQRZM V iff for S, T being object holds
( [S,T] in b2 iff ( S in [: the carrier of V,():] & T in [: the carrier of V,():] & ex z1, z2 being Element of V ex i1, i2 being Element of INT.Ring st
( S = [z1,i1] & T = [z2,i2] & i1 <> 0 & i2 <> 0 & i2 * z1 = i1 * z2 ) ) ) );

theorem LMEQR001: :: ZMODUL04:3
for V being Z_Module
for z1, z2 being Element of V
for i1, i2 being Element of INT.Ring st V is Mult-cancelable holds
( [[z1,i1],[z2,i2]] in EQRZM V iff ( i1 <> 0 & i2 <> 0 & i2 * z1 = i1 * z2 ) )
proof end;

definition
let V be Z_Module;
assume AS: V is Mult-cancelable ;
func addCoset V -> BinOp of (Class ()) means :DefaddCoset: :: ZMODUL04:def 2
for A, B being object st A in Class () & B in Class () holds
for z1, z2 being Element of V
for i1, i2 being Element of INT.Ring st i1 <> 0. INT.Ring & i2 <> 0. INT.Ring & A = Class ((),[z1,i1]) & B = Class ((),[z2,i2]) holds
it . (A,B) = Class ((),[((i2 * z1) + (i1 * z2)),(i1 * i2)]);
existence
ex b1 being BinOp of (Class ()) st
for A, B being object st A in Class () & B in Class () holds
for z1, z2 being Element of V
for i1, i2 being Element of INT.Ring st i1 <> 0. INT.Ring & i2 <> 0. INT.Ring & A = Class ((),[z1,i1]) & B = Class ((),[z2,i2]) holds
b1 . (A,B) = Class ((),[((i2 * z1) + (i1 * z2)),(i1 * i2)])
proof end;
uniqueness
for b1, b2 being BinOp of (Class ()) st ( for A, B being object st A in Class () & B in Class () holds
for z1, z2 being Element of V
for i1, i2 being Element of INT.Ring st i1 <> 0. INT.Ring & i2 <> 0. INT.Ring & A = Class ((),[z1,i1]) & B = Class ((),[z2,i2]) holds
b1 . (A,B) = Class ((),[((i2 * z1) + (i1 * z2)),(i1 * i2)]) ) & ( for A, B being object st A in Class () & B in Class () holds
for z1, z2 being Element of V
for i1, i2 being Element of INT.Ring st i1 <> 0. INT.Ring & i2 <> 0. INT.Ring & A = Class ((),[z1,i1]) & B = Class ((),[z2,i2]) holds
b2 . (A,B) = Class ((),[((i2 * z1) + (i1 * z2)),(i1 * i2)]) ) holds
b1 = b2
proof end;
end;

for V being Z_Module st V is Mult-cancelable holds
for b2 being BinOp of (Class ()) holds
( b2 = addCoset V iff for A, B being object st A in Class () & B in Class () holds
for z1, z2 being Element of V
for i1, i2 being Element of INT.Ring st i1 <> 0. INT.Ring & i2 <> 0. INT.Ring & A = Class ((),[z1,i1]) & B = Class ((),[z2,i2]) holds
b2 . (A,B) = Class ((),[((i2 * z1) + (i1 * z2)),(i1 * i2)]) );

definition
let V be Z_Module;
assume AS: V is Mult-cancelable ;
func zeroCoset V -> Element of Class () means :defZero: :: ZMODUL04:def 3
for i being Integer st i <> 0 holds
it = Class ((),[(0. V),i]);
existence
ex b1 being Element of Class () st
for i being Integer st i <> 0 holds
b1 = Class ((),[(0. V),i])
proof end;
uniqueness
for b1, b2 being Element of Class () st ( for i being Integer st i <> 0 holds
b1 = Class ((),[(0. V),i]) ) & ( for i being Integer st i <> 0 holds
b2 = Class ((),[(0. V),i]) ) holds
b1 = b2
proof end;
end;

:: deftheorem defZero defines zeroCoset ZMODUL04:def 3 :
for V being Z_Module st V is Mult-cancelable holds
for b2 being Element of Class () holds
( b2 = zeroCoset V iff for i being Integer st i <> 0 holds
b2 = Class ((),[(0. V),i]) );

definition
let V be Z_Module;
assume AS: V is Mult-cancelable ;
func lmultCoset V -> Function of [: the carrier of F_Rat,(Class ()):],(Class ()) means :DeflmultCoset: :: ZMODUL04:def 4
for q, A being object st q in RAT & A in Class () holds
for m, n, i being Integer
for mm being Element of INT.Ring
for z being Element of V st m = mm & n <> 0 & q = m / n & i <> 0 & A = Class ((),[z,i]) holds
it . (q,A) = Class ((),[(mm * z),(n * i)]);
existence
ex b1 being Function of [: the carrier of F_Rat,(Class ()):],(Class ()) st
for q, A being object st q in RAT & A in Class () holds
for m, n, i being Integer
for mm being Element of INT.Ring
for z being Element of V st m = mm & n <> 0 & q = m / n & i <> 0 & A = Class ((),[z,i]) holds
b1 . (q,A) = Class ((),[(mm * z),(n * i)])
proof end;
uniqueness
for b1, b2 being Function of [: the carrier of F_Rat,(Class ()):],(Class ()) st ( for q, A being object st q in RAT & A in Class () holds
for m, n, i being Integer
for mm being Element of INT.Ring
for z being Element of V st m = mm & n <> 0 & q = m / n & i <> 0 & A = Class ((),[z,i]) holds
b1 . (q,A) = Class ((),[(mm * z),(n * i)]) ) & ( for q, A being object st q in RAT & A in Class () holds
for m, n, i being Integer
for mm being Element of INT.Ring
for z being Element of V st m = mm & n <> 0 & q = m / n & i <> 0 & A = Class ((),[z,i]) holds
b2 . (q,A) = Class ((),[(mm * z),(n * i)]) ) holds
b1 = b2
proof end;
end;

:: deftheorem DeflmultCoset defines lmultCoset ZMODUL04:def 4 :
for V being Z_Module st V is Mult-cancelable holds
for b2 being Function of [: the carrier of F_Rat,(Class ()):],(Class ()) holds
( b2 = lmultCoset V iff for q, A being object st q in RAT & A in Class () holds
for m, n, i being Integer
for mm being Element of INT.Ring
for z being Element of V st m = mm & n <> 0 & q = m / n & i <> 0 & A = Class ((),[z,i]) holds
b2 . (q,A) = Class ((),[(mm * z),(n * i)]) );

theorem LMEQR003: :: ZMODUL04:4
for V being Z_Module
for z being Element of V
for i, n being Element of INT.Ring st i <> 0. INT.Ring & n <> 0. INT.Ring & V is Mult-cancelable holds
Class ((),[z,i]) = Class ((),[(n * z),(n * i)])
proof end;

theorem LMEQRZM1: :: ZMODUL04:5
for V being Z_Module
for v being Element of ModuleStr(# (Class ()),(),(),() #) st V is Mult-cancelable holds
ex i being Element of INT.Ring ex z being Element of V st
( i <> 0. INT.Ring & v = Class ((),[z,i]) )
proof end;

ThEQRZMV1: for V being Z_Module st V is Mult-cancelable holds
ModuleStr(# (Class ()),(),(),() #) is VectSp of F_Rat

proof end;

definition
let V be Z_Module;
assume AS: V is Mult-cancelable ;
func Z_MQ_VectSp V -> VectSp of F_Rat equals :defZMQVSp: :: ZMODUL04:def 5
ModuleStr(# (Class ()),(),(),() #);
correctness
coherence
ModuleStr(# (Class ()),(),(),() #) is VectSp of F_Rat
;
by ;
end;

:: deftheorem defZMQVSp defines Z_MQ_VectSp ZMODUL04:def 5 :
for V being Z_Module st V is Mult-cancelable holds
Z_MQ_VectSp V = ModuleStr(# (Class ()),(),(),() #);

ThEQRZMV2: for V being Z_Module st V is Mult-cancelable holds
ex I being Function of V,() st
( I is one-to-one & ( for v being Element of V holds I . v = Class ((),[v,1]) ) & ( for v, w being Element of V holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Element of V
for i being Element of INT.Ring
for q being Element of F_Rat st i = q holds
I . (i * v) = q * (I . v) ) & I . (0. V) = 0. () )

proof end;

definition
let V be Z_Module;
assume AS: V is Mult-cancelable ;
func MorphsZQ V -> Function of V,() means :defMorph: :: ZMODUL04:def 6
( it is one-to-one & ( for v being Element of V holds it . v = Class ((),[v,1]) ) & ( for v, w being Element of V holds it . (v + w) = (it . v) + (it . w) ) & ( for v being Element of V
for i being Element of INT.Ring
for q being Element of F_Rat st i = q holds
it . (i * v) = q * (it . v) ) & it . (0. V) = 0. () );
existence
ex b1 being Function of V,() st
( b1 is one-to-one & ( for v being Element of V holds b1 . v = Class ((),[v,1]) ) & ( for v, w being Element of V holds b1 . (v + w) = (b1 . v) + (b1 . w) ) & ( for v being Element of V
for i being Element of INT.Ring
for q being Element of F_Rat st i = q holds
b1 . (i * v) = q * (b1 . v) ) & b1 . (0. V) = 0. () )
by ;
uniqueness
for b1, b2 being Function of V,() st b1 is one-to-one & ( for v being Element of V holds b1 . v = Class ((),[v,1]) ) & ( for v, w being Element of V holds b1 . (v + w) = (b1 . v) + (b1 . w) ) & ( for v being Element of V
for i being Element of INT.Ring
for q being Element of F_Rat st i = q holds
b1 . (i * v) = q * (b1 . v) ) & b1 . (0. V) = 0. () & b2 is one-to-one & ( for v being Element of V holds b2 . v = Class ((),[v,1]) ) & ( for v, w being Element of V holds b2 . (v + w) = (b2 . v) + (b2 . w) ) & ( for v being Element of V
for i being Element of INT.Ring
for q being Element of F_Rat st i = q holds
b2 . (i * v) = q * (b2 . v) ) & b2 . (0. V) = 0. () holds
b1 = b2
proof end;
end;

:: deftheorem defMorph defines MorphsZQ ZMODUL04:def 6 :
for V being Z_Module st V is Mult-cancelable holds
for b2 being Function of V,() holds
( b2 = MorphsZQ V iff ( b2 is one-to-one & ( for v being Element of V holds b2 . v = Class ((),[v,1]) ) & ( for v, w being Element of V holds b2 . (v + w) = (b2 . v) + (b2 . w) ) & ( for v being Element of V
for i being Element of INT.Ring
for q being Element of F_Rat st i = q holds
b2 . (i * v) = q * (b2 . v) ) & b2 . (0. V) = 0. () ) );

theorem XThSum: :: ZMODUL04:6
for V being Z_Module st V is Mult-cancelable holds
for s being FinSequence of V
for t being FinSequence of () st len s = len t & ( for i being Element of NAT st i in dom s holds
ex si being Vector of V st
( si = s . i & t . i = () . si ) ) holds
Sum t = () . (Sum s)
proof end;

theorem XThSum1: :: ZMODUL04:7
for V being Z_Module
for I being Subset of V
for IQ being Subset of ()
for l being Linear_Combination of I
for lq being Linear_Combination of IQ st V is Mult-cancelable & IQ = () .: I & l = lq * () holds
Sum lq = () . (Sum l)
proof end;

theorem ThEQRZMV3A: :: ZMODUL04:8
for V being Z_Module
for IQ being Subset of ()
for lq being Linear_Combination of IQ ex m being Integer ex a being Element of F_Rat st
( m <> 0 & m = a & rng (a * lq) c= INT )
proof end;

theorem ThEQRZMV3: :: ZMODUL04:9
for V being Z_Module
for I being Subset of V
for IQ being Subset of ()
for lq being Linear_Combination of IQ st V is Mult-cancelable & IQ = () .: I holds
ex m being Element of INT.Ring ex a being Element of F_Rat ex l being Linear_Combination of I st
( m <> 0. INT.Ring & m = a & l = (a * lq) * () & () " (Carrier lq) = Carrier l )
proof end;

theorem ThEQRZMV3B: :: ZMODUL04:10
for V being Z_Module
for I being Subset of V
for IQ being Subset of ()
for lq being Linear_Combination of IQ
for m being Integer
for a being Element of F_Rat
for l being Linear_Combination of I st V is Mult-cancelable & IQ = () .: I & m <> 0 & m = a & l = (a * lq) * () holds
a * (Sum lq) = () . (Sum l)
proof end;

theorem ThEQRZMV3C: :: ZMODUL04:11
for V being Z_Module
for I being Subset of V
for IQ being Subset of () st V is Mult-cancelable & IQ = () .: I & I is linearly-independent holds
IQ is linearly-independent
proof end;

theorem ThEQRZMV4: :: ZMODUL04:12
for V being Z_Module
for I being Subset of V
for l being Linear_Combination of I
for IQ being Subset of () st V is Mult-cancelable & IQ = () .: I holds
ex lq being Linear_Combination of IQ st
( l = lq * () & Carrier lq = () .: () )
proof end;

theorem ThQuotAX: :: ZMODUL04:13
for V being free Z_Module
for I being Subset of V
for IQ being Subset of ()
for l being Linear_Combination of I
for i being Element of INT.Ring st i <> 0. INT.Ring & IQ = () .: I holds
Class ((),[(Sum l),i]) in Lin IQ
proof end;

theorem ThEQRZMV3E: :: ZMODUL04:14
for V being free Z_Module
for I being Subset of V
for IQ being Subset of () st IQ = () .: I holds
card I = card IQ
proof end;

theorem ThEQRZMV3D: :: ZMODUL04:15
for V being free Z_Module
for I being Subset of V
for IQ being Subset of () st IQ = () .: I & I is Basis of V holds
IQ is Basis of ()
proof end;

registration
let V be free finite-rank Z_Module;
coherence
proof end;
end;

theorem :: ZMODUL04:16
for V being free finite-rank Z_Module holds rank V = dim ()
proof end;

theorem XXTh1: :: ZMODUL04:17
for V being free Z_Module
for I, A being finite Subset of V st I is Basis of V & (card I) + 1 = card A holds
A is linearly-dependent
proof end;

theorem XXTh2: :: ZMODUL04:18
for V being free Z_Module
for A, B being Subset of V st A is linearly-dependent & A c= B holds
B is linearly-dependent by VECTSP_7:1;

theorem XXTh3: :: ZMODUL04:19
for V being free Z_Module
for D, A being Subset of V st D is Basis of V & D is finite & card D c< card A holds
A is linearly-dependent
proof end;

theorem :: ZMODUL04:20
for V being free Z_Module
for I, A being Subset of V st I is Basis of V & I is finite & A is linearly-independent holds
card A c= card I by ;

theorem :: ZMODUL04:21
for V being Z_Module st (Omega). V is free holds
V is free
proof end;

theorem :: ZMODUL04:22
for R being Ring
for V being LeftMod of R
for W1, W2 being Subspace of V
for W1s, W2s being strict Subspace of V st W1s = (Omega). W1 & W2s = (Omega). W2 holds
W1s + W2s = W1 + W2
proof end;

theorem :: ZMODUL04:23
for R being Ring
for V being LeftMod of R
for W1, W2 being Subspace of V
for W1s, W2s being strict Subspace of V st W1s = (Omega). W1 & W2s = (Omega). W2 holds
W1s /\ W2s = W1 /\ W2
proof end;

theorem Thn0V: :: ZMODUL04:24
for R being Ring
for V being LeftMod of R
for W being strict Subspace of V st W <> (0). V holds
ex v being Vector of V st
( v in W & v <> 0. V )
proof end;

theorem ThCarrier1: :: ZMODUL04:25
for K being Ring
for V being VectSp of K
for A being Subset of V
for l1, l2 being Linear_Combination of A st (Carrier l1) /\ (Carrier l2) = {} holds
Carrier (l1 + l2) = (Carrier l1) \/ (Carrier l2)
proof end;

theorem ThCarrier2: :: ZMODUL04:26
for R being Ring
for V being VectSp of R
for A1, A2 being Subset of V
for l being Linear_Combination of A1 \/ A2 st A1 /\ A2 = {} holds
ex l1 being Linear_Combination of A1 ex l2 being Linear_Combination of A2 st l = l1 + l2
proof end;

theorem FRds1: :: ZMODUL04:27
for V being Z_Module
for W1, W2 being free Subspace of V
for I1 being Basis of W1
for I2 being Basis of W2 st V is_the_direct_sum_of W1,W2 holds
I1 /\ I2 = {}
proof end;

theorem FRds2: :: ZMODUL04:28
for V being Z_Module
for W1, W2 being free Subspace of V
for I1 being Basis of W1
for I2 being Basis of W2
for I being Subset of V st V is_the_direct_sum_of W1,W2 & I = I1 \/ I2 holds
Lin I = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #)
proof end;

theorem FRds3: :: ZMODUL04:29
for V being LeftMod of INT.Ring
for W1, W2 being free Subspace of V
for I1 being Basis of W1
for I2 being Basis of W2
for I being Subset of V st V is_the_direct_sum_of W1,W2 & I = I1 \/ I2 holds
I is linearly-independent
proof end;

theorem FRdsX: :: ZMODUL04:30
for V being Z_Module
for W1, W2 being free Subspace of V st V is_the_direct_sum_of W1,W2 holds
V is free
proof end;

theorem ThDirectSum: :: ZMODUL04:31
for V being Z_Module
for W1, W2 being free Subspace of V st W1 /\ W2 = (0). V holds
W1 + W2 is free
proof end;

theorem :: ZMODUL04:32
for V being free Z_Module
for I being Basis of V
for v being Vector of V st v in I holds
( Lin (I \ {v}) is free & Lin {v} is free )
proof end;

theorem FRdsY: :: ZMODUL04:33
for V being free Z_Module
for I being Basis of V
for v being Vector of V st v in I holds
V is_the_direct_sum_of Lin (I \ {v}), Lin {v}
proof end;

FRX: for V being free finite-rank Z_Module
for W being Subspace of V holds W is free

proof end;

registration
let V be free finite-rank Z_Module;
cluster -> free for Subspace of V;
correctness
coherence
for b1 being Subspace of V holds b1 is free
;
by FRX;
end;

theorem :: ZMODUL04:34
for V being Z_Module
for W being Subspace of V
for W1, W2 being free Subspace of V st W1 /\ W2 = (0). V & ModuleStr(# the carrier of W, the addF of W, the ZeroF of W, the lmult of W #) = W1 + W2 holds
W is free
proof end;

theorem :: ZMODUL04:35
for p being prime Element of INT.Ring
for V being free Z_Module st Z_MQ_VectSp (V,p) is finite-dimensional holds
V is finite-rank
proof end;

theorem :: ZMODUL04:36
for p being prime Element of INT.Ring
for V being Z_Module
for s being Element of V
for a being Element of INT.Ring
for b being Element of (GF p) st b = a mod p holds
b * (ZMtoMQV (V,p,s)) = ZMtoMQV (V,p,(a * s))
proof end;

LMX2: for p being prime Element of INT.Ring
for V being free Z_Module
for i being Element of INT.Ring
for v being Element of V holds ZMtoMQV (V,p,((i mod p) * v)) = ZMtoMQV (V,p,(i * v))

proof end;

theorem ThQuotBasis5A: :: ZMODUL04:37
for p being prime Element of INT.Ring
for V being free Z_Module
for I being Subset of V
for IQ being Subset of (Z_MQ_VectSp (V,p))
for l being Linear_Combination of I st IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } holds
ZMtoMQV (V,p,(Sum l)) in Lin IQ
proof end;

theorem ThQuotBasis5: :: ZMODUL04:38
for p being prime Element of INT.Ring
for V being free Z_Module
for I being Subset of V
for IQ being Subset of (Z_MQ_VectSp (V,p)) st Lin I = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) & IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } holds
Lin IQ = ModuleStr(# the carrier of (Z_MQ_VectSp (V,p)), the addF of (Z_MQ_VectSp (V,p)), the ZeroF of (Z_MQ_VectSp (V,p)), the lmult of (Z_MQ_VectSp (V,p)) #)
proof end;

theorem FG02: :: ZMODUL04:39
for V being free finitely-generated Z_Module ex A being finite Subset of V st A is Basis of V
proof end;

registration
coherence
for b1 being free finitely-generated Z_Module holds b1 is finite-rank
proof end;
end;

registration
coherence
for b1 being free finite-rank Z_Module holds b1 is finitely-generated
proof end;
end;

theorem RL5Th25: :: ZMODUL04:40
for V being free finite-rank Z_Module
for A being Subset of V st A is linearly-independent holds
A is finite
proof end;

RL5Th28: for V being free finite-rank Z_Module
for W being Subspace of V holds W is finite-rank

proof end;

registration
let V be Z_Module;
let W1, W2 be free finite-rank Subspace of V;
cluster W1 /\ W2 -> free ;
correctness
coherence
W1 /\ W2 is free
;
proof end;
end;

registration
let V be Z_Module;
let W1, W2 be free finite-rank Subspace of V;
cluster W1 /\ W2 -> finite-rank ;
correctness
coherence
W1 /\ W2 is finite-rank
;
proof end;
end;

registration
let V be free finite-rank Z_Module;
cluster -> finite-rank for Subspace of V;
correctness
coherence
for b1 being Subspace of V holds b1 is finite-rank
;
by RL5Th28;
end;