let m be integer-yielding FinSequence; :: thesis: for i, j being natural number st i in dom m & j in dom m & j <> i & m . j <> 0 holds
ex z being Integer st z * (m . i) = (Product m) / (m . j)
let i9, j9 be natural number ; :: thesis: ( i9 in dom m & j9 in dom m & j9 <> i9 & m . j9 <> 0 implies ex z being Integer st z * (m . i9) = (Product m) / (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) = (Product m) / (m . j9)
reconsider i = i9, j = j9 as Element of NAT by ORDINAL1:def 13;
A5: dom m = Seg (len m) by FINSEQ_1:def 3;
then A6: j <= len m by A2, FINSEQ_1:3;
A7: 1 <= j by A2, A5, FINSEQ_1:3;
then 1 - 1 <= j - 1 by XREAL_1:11;
then reconsider kj = j - 1 as Element of NAT by INT_1:16;
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 A6, FINSEQ_1:80, XXREAL_0:2;
A9: dom m = Seg (len m) by FINSEQ_1:def 3;
then A10: 1 <= i by A1, FINSEQ_1:3;
then 1 - 1 <= i - 1 by XREAL_1:11;
then reconsider ki = i - 1 as Element of NAT by INT_1:16;
A11: i <= len m by A1, A9, FINSEQ_1:3;
ex l being Element of NAT st
( l in dom f & f . l = m . i )

proof

per cases ( i < j or i > j ) by A3, XXREAL_0:1;

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:39;
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 A8, FINSEQ_1:def 3;
then (m | kj) . i = m . i by FUNCT_1:70;
then f . i = m . i by A14, FINSEQ_1:def 7;
hence ex l being Element of NAT st
( l in dom f & f . l = m . i ) by A14, A13; :: 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:11;
then reconsider a = (i - 1) - kj as Element of NAT by INT_1:18;
i - kj > (kj + 1) - kj by A15, XREAL_1:11;
then (i - kj) - 1 > 1 - 1 by XREAL_1:11;
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 A6, RFINSEQ:def 2;
then len f = kj + ((len m) - j) by A8, FINSEQ_1:35
.= (len m) - 1 ;
then A18: ki <= len f by A11, XREAL_1:11;
i - j <= (len m) - j by A11, XREAL_1:11;
then a in Seg (len (m /^ j)) by A17, A16;
then A19: (i - 1) - kj in dom (m9 /^ j) by FINSEQ_1:def 3;
ki + 1 > 1 by A7, A15, XXREAL_0:2;
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;
len (m | kj) < i - 1 by A8, A15, XREAL_1:11;
then f . ki = (m /^ j) . (ki - kj) by A8, A18, FINSEQ_1:37
.= (m9 /^ j) /. (ki - kj) by A19, PARTFUN1:def 8
.= m9 /. (j + a) by A19, FINSEQ_5:30
.= m . i by A1, PARTFUN1:def 8 ;
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 A21, FINSEQ_1:def 3;
then 1 <= l by FINSEQ_1:3;
then reconsider kl = l - 1 as Element of NAT by INT_1:18;
l in Seg (len f) by A21, FINSEQ_1:def 3;
then kl + 1 <= len f by FINSEQ_1:3;
then (f | kl) ^ <*(f . l)*> = f | l by Th5;
then f = ((f | kl) ^ <*(f . l)*>) ^ (f /^ l) by RFINSEQ:21;
then A23: Product f = (Product ((f | kl) ^ <*(f . l)*>)) * (Product (f /^ l)) by RVSUM_1:127
.= ((Product (f | kl)) * (Product <*(f . l)*>)) * (Product (f /^ l)) by RVSUM_1:127
.= ((Product (f | kl)) * (Product (f /^ l))) * (Product <*(m . i)*>) by A22
.= ((Product (f | kl)) * (Product (f /^ l))) * (m . i) by RVSUM_1:125
.= (Product ((f | kl) ^ (f /^ l))) * (m . i) by RVSUM_1:127 ;
kj + 1 <= len m by A2, A5, FINSEQ_1:3;
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:21;
then Product m = (Product ((m | kj) ^ <*(m . j)*>)) * (Product (m /^ j)) by A24, RVSUM_1:127
.= ((Product (m | kj)) * (Product <*(m . j)*>)) * (Product (m /^ j)) by RVSUM_1:127
.= ((Product (m | kj)) * (Product (m /^ j))) * (Product <*(m . j)*>)
.= ((Product (m | kj)) * (Product (m /^ j))) * (m . j) by RVSUM_1:125
.= (Product f) * (m . j) by RVSUM_1:127 ;
then (Product m) / (m . j) = (Product f) * ((m . j) * ((m . j) "))
.= (Product f) * 1 by A4, XCMPLX_0:def 7 ;
hence ex z being Integer st z * (m . i9) = (Product m) / (m . j9) by A23; :: thesis: verum