let V be Z_Module; :: thesis: 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 )

let IQ be Subset of (); :: thesis: 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 )

defpred S1[ Nat] means for lq being Linear_Combination of IQ st card (Carrier lq) = \$1 holds
ex m being Integer ex a being Element of F_Rat st
( m <> 0 & m = a & rng (a * lq) c= INT );
P1: S1[ 0 ]
proof
let lq be Linear_Combination of IQ; :: thesis: ( card (Carrier lq) = 0 implies ex m being Integer ex a being Element of F_Rat st
( m <> 0 & m = a & rng (a * lq) c= INT ) )

assume P2: card (Carrier lq) = 0 ; :: thesis: ex m being Integer ex a being Element of F_Rat st
( m <> 0 & m = a & rng (a * lq) c= INT )

P3: Carrier lq = {} by P2;
reconsider m = 1 as Integer ;
reconsider a = m as Element of F_Rat ;
Carrier (a * lq) c= Carrier lq by VECTSP_6:28;
then Carrier (a * lq) = {} by P3;
then X1: a * lq = ZeroLC () by VECTSP_6:def 3;
now :: thesis: for y being object st y in rng (a * lq) holds
y in INT
let y be object ; :: thesis: ( y in rng (a * lq) implies y in INT )
assume y in rng (a * lq) ; :: thesis:
then consider x being Element of () such that
X2: y = (a * lq) . x by FUNCT_2:113;
(a * lq) . x = 0. F_Rat by
.= 0 ;
hence y in INT by X2; :: thesis: verum
end;
hence ex m being Integer ex a being Element of F_Rat st
( m <> 0 & m = a & rng (a * lq) c= INT ) by TARSKI:def 3; :: thesis: verum
end;
P2: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume P21: S1[n] ; :: thesis: S1[n + 1]
now :: thesis: for lq being Linear_Combination of IQ st card (Carrier lq) = n + 1 holds
ex m being Integer ex a being Element of F_Rat st
( m <> 0 & m = a & rng (a * lq) c= INT )
let lq be Linear_Combination of IQ; :: thesis: ( card (Carrier lq) = n + 1 implies ex m being Integer ex a being Element of F_Rat st
( m <> 0 & m = a & rng (a * lq) c= INT ) )

assume P22: card (Carrier lq) = n + 1 ; :: thesis: ex m being Integer ex a being Element of F_Rat st
( m <> 0 & m = a & rng (a * lq) c= INT )

then Carrier lq <> {} ;
then consider x being object such that
P24: x in Carrier lq by XBOOLE_0:def 1;
reconsider x = x as Element of () by P24;
P25: card ((Carrier lq) \ {x}) = (card (Carrier lq)) - () by
.= (n + 1) - 1 by
.= n ;
defpred S2[ Element of (), Element of F_Rat] means ( ( \$1 in {x} implies \$2 = 0 ) & ( not \$1 in {x} implies \$2 = lq . \$1 ) );
A2: for v being Element of () ex y being Element of F_Rat st S2[v,y]
proof
let v be Element of (); :: thesis: ex y being Element of F_Rat st S2[v,y]
( v in {x} or not v in {x} ) ;
hence ex y being Element of F_Rat st S2[v,y] ; :: thesis: verum
end;
consider lq0 being Function of the carrier of (), the carrier of F_Rat such that
A4: for v being Element of () holds S2[v,lq0 . v] from reconsider lq0 = lq0 as Element of Funcs ( the carrier of (), the carrier of F_Rat) by FUNCT_2:8;
set T = { v where v is Element of () : lq0 . v <> 0. F_Rat } ;
A400: { v where v is Element of () : lq0 . v <> 0. F_Rat } c= (Carrier lq) \ {x}
proof
let v0 be object ; :: according to TARSKI:def 3 :: thesis: ( not v0 in { v where v is Element of () : lq0 . v <> 0. F_Rat } or v0 in (Carrier lq) \ {x} )
assume v0 in { v where v is Element of () : lq0 . v <> 0. F_Rat } ; :: thesis: v0 in (Carrier lq) \ {x}
then XX2: ex v1 being Element of () st
( v1 = v0 & lq0 . v1 <> 0. F_Rat ) ;
then reconsider v = v0 as Element of () ;
XX4: not v in {x} by ;
lq . v <> 0. F_Rat by ;
then v0 in Carrier lq ;
hence v0 in (Carrier lq) \ {x} by ; :: thesis: verum
end;
(Carrier lq) \ {x} c= Carrier lq by XBOOLE_1:36;
then A40: { v where v is Element of () : lq0 . v <> 0. F_Rat } c= Carrier lq by ;
reconsider T = { v where v is Element of () : lq0 . v <> 0. F_Rat } as finite Subset of () by ;
for v being Element of () st not v in T holds
lq0 . v = 0. F_Rat ;
then reconsider lq0 = lq0 as Linear_Combination of Z_MQ_VectSp V by VECTSP_6:def 1;
X5: T = Carrier lq0 ;
Carrier lq c= IQ by VECTSP_6:def 4;
then reconsider lq0 = lq0 as Linear_Combination of IQ by ;
(Carrier lq) \ {x} c= T
proof
let v0 be object ; :: according to TARSKI:def 3 :: thesis: ( not v0 in (Carrier lq) \ {x} or v0 in T )
assume YY11: v0 in (Carrier lq) \ {x} ; :: thesis: v0 in T
then YY1: ( v0 in Carrier lq & not v0 in {x} ) by XBOOLE_0:def 5;
reconsider v = v0 as Element of () by YY11;
lq . v <> 0. F_Rat by ;
then lq0 . v <> 0. F_Rat by ;
hence v0 in T ; :: thesis: verum
end;
then card (Carrier lq0) = n by ;
then consider m0 being Integer, a0 being Element of F_Rat such that
X8: ( m0 <> 0 & m0 = a0 & rng (a0 * lq0) c= INT ) by P21;
consider k0, n0 being Integer such that
X9: ( n0 <> 0 & lq . x = k0 / n0 ) by RAT_1:1;
reconsider m = n0 * m0 as Integer ;
reconsider a = m as Element of F_Rat by RAT_1:def 2;
reconsider b = n0 as Element of F_Rat by RAT_1:def 2;
for y being object st y in rng (a * lq) holds
y in INT
proof
let y be object ; :: thesis: ( y in rng (a * lq) implies y in INT )
assume y in rng (a * lq) ; :: thesis:
then consider z being Element of () such that
X2: y = (a * lq) . z by FUNCT_2:113;
per cases ( z in {x} or not z in {x} ) ;
suppose B2: z in {x} ; :: thesis:
BB2: y = (a * lq) . x by
.= a * (lq . x) by VECTSP_6:def 9 ;
a * (lq . x) = (m0 * n0) * (k0 / n0) by X9
.= m0 * (n0 * (k0 / n0))
.= m0 * k0 by ;
hence y in INT by ; :: thesis: verum
end;
suppose not z in {x} ; :: thesis:
then B31: lq0 . z = lq . z by A4;
BBB: a = b * a0 by X8;
B32: (a * lq) . z = a * (lq . z) by VECTSP_6:def 9
.= b * (a0 * (lq0 . z)) by
.= b * ((a0 * lq0) . z) by VECTSP_6:def 9 ;
(a0 * lq0) . z in rng (a0 * lq0) by FUNCT_2:4;
then reconsider aqz = (a0 * lq0) . z as Integer by X8;
b * ((a0 * lq0) . z) = n0 * aqz ;
hence y in INT by ; :: thesis: verum
end;
end;
end;
hence ex m being Integer ex a being Element of F_Rat st
( m <> 0 & m = a & rng (a * lq) c= INT ) by ; :: thesis: verum
end;
hence S1[n + 1] ; :: thesis: verum
end;
P3: for n being Nat holds S1[n] from NAT_1:sch 2(P1, P2);
now :: thesis: 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 )
let lq be Linear_Combination of IQ; :: thesis: ex m being Integer ex a being Element of F_Rat st
( m <> 0 & m = a & rng (a * lq) c= INT )

card (Carrier lq) is Element of NAT ;
hence ex m being Integer ex a being Element of F_Rat st
( m <> 0 & m = a & rng (a * lq) c= INT ) by P3; :: thesis: verum
end;
hence 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 ) ; :: thesis: verum