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 i', j' be natural number ; :: thesis: ( i' in dom m & j' in dom m & j' <> i' & m . j' <> 0 implies ex z being Integer st z * (m . i') = (Product m) / (m . j') )
assume AS: ( i' in dom m & j' in dom m & j' <> i' & m . j' <> 0 ) ; :: thesis: ex z being Integer st z * (m . i') = (Product m) / (m . j')
reconsider i = i', j = j' as Element of NAT by ORDINAL1:def 13;
reconsider mj = (Product m) / (m . j') as Integer by AS, prodint;
dom m = Seg (len m) by FINSEQ_1:def 3;
then X1: ( 1 <= i & i <= len m ) by AS, 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;
A3: dom m = Seg (len m) by FINSEQ_1:def 3;
then X2: ( 1 <= j & j <= len m ) by AS, 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 m' = m as FinSequence of INT by intint;
reconsider m1 = m | j as FinSequence of INT by intint;
reconsider m2 = m /^ j as FinSequence of INT by intint;
reconsider f = (m | kj) ^ (m /^ j) as FinSequence of INT by intint;
kj + 1 <= len m by A3, AS, FINSEQ_1:3;
then X: (m | kj) ^ <*(m . j)*> = m | j by th67;
m' = m1 ^ m2 by RFINSEQ:21;
then Product m = (Product ((m | kj) ^ <*(m . j)*>)) * (Product (m /^ j)) by X, 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 X: (Product m) / (m . j) = (Product f) * ((m . j) * ((m . j) " ))
.= (Product f) * 1 by AS, XCMPLX_0:def 7 ;
kj + 1 = j ;
then kj <= j by NAT_1:11;
then Y1: len (m | kj) = kj by X2, FINSEQ_1:80, XXREAL_0:2;
ex l being Element of NAT st
( l in dom f & f . l = m . i )

proof

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

suppose i < j ; :: thesis: ex l being Element of NAT st
( l in dom f & f . l = m . i )

then i < kj + 1 ;
then i <= j - 1 by NAT_1:13;
then i in Seg kj by X1;
then Z1: i in dom (m | kj) by Y1, FINSEQ_1:def 3;
Z2: dom (m | kj) c= dom f by FINSEQ_1:39;
(m | kj) . i = m . i by Z1, FUNCT_1:70;
then f . i = m . i by Z1, FINSEQ_1:def 7;
hence ex l being Element of NAT st
( l in dom f & f . l = m . i ) by Z2, Z1; :: thesis: verum

end;

suppose ZZ: i > j ; :: thesis: ex l being Element of NAT st
( l in dom f & f . l = m . i )

then ki + 1 > 1 by X2, XXREAL_0:2;
then Y4: ki >= 1 by NAT_1:13;
Z3: len (m /^ j) = (len m) - j by X2, RFINSEQ:def 2;
then Z4: len f = kj + ((len m) - j) by Y1, FINSEQ_1:35
.= (len m) - 1 ;
Y2: ki <= len f by X1, Z4, XREAL_1:11;
then ki in Seg (len f) by Y4;
then Y3: ki in dom f by FINSEQ_1:def 3;
i - 1 > kj by ZZ, XREAL_1:11;
then reconsider a = (i - 1) - kj as Element of NAT by INT_1:18;
i - kj > (kj + 1) - kj by ZZ, 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 Z2: 1 <= (i - 1) - kj by NAT_1:11;
i - j <= (len m) - j by X1, XREAL_1:11;
then a in Seg (len (m /^ j)) by Z2, Z3;
then Z1: (i - 1) - kj in dom (m' /^ j) by FINSEQ_1:def 3;
len (m | kj) < i - 1 by ZZ, Y1, XREAL_1:11;
then f . ki = (m /^ j) . (ki - kj) by Y1, Y2, FINSEQ_1:37
.= (m' /^ j) /. (ki - kj) by Z1, PARTFUN1:def 8
.= m' /. (j + a) by Z1, FINSEQ_5:30
.= m . i by AS, PARTFUN1:def 8 ;
hence ex l being Element of NAT st
( l in dom f & f . l = m . i ) by Y3; :: thesis: verum

end;

end;

end;

then consider l being Element of NAT such that
Y: ( l in dom f & f . l = m . i ) ;
l in Seg (len f) by Y, 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 Y, FINSEQ_1:def 3;
then kl + 1 <= len f by FINSEQ_1:3;
then (f | kl) ^ <*(f . l)*> = f | l by th67;
then f = ((f | kl) ^ <*(f . l)*>) ^ (f /^ l) by RFINSEQ:21;
then 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 Y
.= ((Product (f | kl)) * (Product (f /^ l))) * (m . i) by RVSUM_1:125
.= (Product ((f | kl) ^ (f /^ l))) * (m . i) by RVSUM_1:127 ;
hence ex z being Integer st z * (m . i') = (Product m) / (m . j') by X; :: thesis: verum