let m be INT -valued FinSequence; :: thesis: for i, j being Nat st i in dom m & j in dom m & j <> i & m . j <> 0 holds
ex z being Integer st z * (m . i) = () / (m . j)

let i9, j9 be Nat; :: thesis: ( i9 in dom m & j9 in dom m & j9 <> i9 & m . j9 <> 0 implies ex z being Integer st z * (m . i9) = () / (m . j9) )
reconsider m9 = m as FinSequence of INT by Lm1;
assume that
A1: i9 in dom m and
A2: j9 in dom m and
A3: j9 <> i9 and
A4: m . j9 <> 0 ; :: thesis: ex z being Integer st z * (m . i9) = () / (m . j9)
reconsider i = i9, j = j9 as Element of NAT by ORDINAL1:def 12;
A5: dom m = Seg (len m) by FINSEQ_1:def 3;
then A6: j <= len m by ;
A7: 1 <= j by ;
then 1 - 1 <= j - 1 by XREAL_1:9;
then reconsider kj = j - 1 as Element of NAT by INT_1:3;
set f = (m | kj) ^ (m /^ j);
reconsider f = (m | kj) ^ (m /^ j) as FinSequence of INT by Lm1;
kj + 1 = j ;
then kj <= j by NAT_1:11;
then A8: len (m | kj) = kj by ;
A9: dom m = Seg (len m) by FINSEQ_1:def 3;
then A10: 1 <= i by ;
then 1 - 1 <= i - 1 by XREAL_1:9;
then reconsider ki = i - 1 as Element of NAT by INT_1:3;
A11: i <= len m by ;
ex l being Element of NAT st
( l in dom f & f . l = m . i )
proof
per cases ( i < j or i > j ) by ;
suppose A12: i < j ; :: thesis: ex l being Element of NAT st
( l in dom f & f . l = m . i )

A13: dom (m | kj) c= dom f by FINSEQ_1:26;
i < kj + 1 by A12;
then i <= j - 1 by NAT_1:13;
then i in Seg kj by A10;
then A14: i in dom (m | kj) by ;
then (m | kj) . i = m . i by FUNCT_1:47;
then f . i = m . i by ;
hence ex l being Element of NAT st
( l in dom f & f . l = m . i ) by ; :: thesis: verum
end;
suppose A15: i > j ; :: thesis: ex l being Element of NAT st
( l in dom f & f . l = m . i )

then i - 1 > kj by XREAL_1:9;
then reconsider a = (i - 1) - kj as Element of NAT by INT_1:5;
i - kj > (kj + 1) - kj by ;
then (i - kj) - 1 > 1 - 1 by XREAL_1:9;
then ex g being Nat st a = g + 1 by NAT_1:6;
then A16: 1 <= (i - 1) - kj by NAT_1:11;
A17: len (m /^ j) = (len m) - j by ;
then len f = kj + ((len m) - j) by
.= (len m) - 1 ;
then A18: ki <= len f by ;
i - j <= (len m) - j by ;
then a in Seg (len (m /^ j)) by ;
then A19: (i - 1) - kj in dom (m9 /^ j) by FINSEQ_1:def 3;
ki + 1 > 1 by ;
then ki >= 1 by NAT_1:13;
then ki in Seg (len f) by A18;
then A20: ki in dom f by FINSEQ_1:def 3;
reconsider D = INT as set ;
reconsider ww = m9 as FinSequence of D ;
len (m | kj) < i - 1 by ;
then f . ki = (m /^ j) . (ki - kj) by
.= (ww /^ j) /. (ki - kj) by
.= ww /. (j + a) by
.= m . i by ;
hence ex l being Element of NAT st
( l in dom f & f . l = m . i ) by A20; :: thesis: verum
end;
end;
end;
then consider l being Element of NAT such that
A21: l in dom f and
A22: f . l = m . i ;
l in Seg (len f) by ;
then 1 <= l by FINSEQ_1:1;
then reconsider kl = l - 1 as Element of NAT by INT_1:5;
l in Seg (len f) by ;
then kl + 1 <= len f by FINSEQ_1:1;
then (f | kl) ^ <*(f . l)*> = f | l by Th5;
then f = ((f | kl) ^ <*(f . l)*>) ^ (f /^ l) by RFINSEQ:8;
then A23: Product f = (Product ((f | kl) ^ <*(f . l)*>)) * (Product (f /^ l)) by RVSUM_1:97
.= ((Product (f | kl)) * (Product <*(f . l)*>)) * (Product (f /^ l)) by RVSUM_1:97
.= ((Product (f | kl)) * (Product (f /^ l))) * (Product <*(m . i)*>) by A22
.= ((Product (f | kl)) * (Product (f /^ l))) * (m . i)
.= (Product ((f | kl) ^ (f /^ l))) * (m . i) by RVSUM_1:97 ;
kj + 1 <= len m by ;
then A24: (m | kj) ^ <*(m . j)*> = m | j by Th5;
reconsider m2 = m /^ j as FinSequence of INT by Lm1;
reconsider m1 = m | j as FinSequence of INT by Lm1;
m9 = m1 ^ m2 by RFINSEQ:8;
then Product m = (Product ((m | kj) ^ <*(m . j)*>)) * (Product (m /^ j)) by
.= ((Product (m | kj)) * (Product <*(m . j)*>)) * (Product (m /^ j)) by RVSUM_1:97
.= ((Product (m | kj)) * (Product (m /^ j))) * (Product <*(m . j)*>)
.= ((Product (m | kj)) * (Product (m /^ j))) * (m . j)
.= () * (m . j) by RVSUM_1:97 ;
then () / (m . j) = () * ((m . j) * ((m . j) "))
.= () * 1 by ;
hence ex z being Integer st z * (m . i9) = () / (m . j9) by A23; :: thesis: verum