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) = (Product m) / (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) = (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 12;

A5: dom m = Seg (len m) by FINSEQ_1:def 3;

then A6: j <= len m by A2, FINSEQ_1:1;

A7: 1 <= j by A2, A5, FINSEQ_1:1;

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 A6, FINSEQ_1:59, XXREAL_0:2;

A9: dom m = Seg (len m) by FINSEQ_1:def 3;

then A10: 1 <= i by A1, FINSEQ_1:1;

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 A1, A9, FINSEQ_1:1;

ex l being Element of NAT st

( l in dom f & f . l = m . i )

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:1;

then reconsider kl = l - 1 as Element of NAT by INT_1:5;

l in Seg (len f) by A21, FINSEQ_1:def 3;

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 A2, A5, FINSEQ_1:1;

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 A24, RVSUM_1:97

.= ((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)

.= (Product f) * (m . j) by RVSUM_1:97 ;

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

ex z being Integer st z * (m . i) = (Product m) / (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) = (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 12;

A5: dom m = Seg (len m) by FINSEQ_1:def 3;

then A6: j <= len m by A2, FINSEQ_1:1;

A7: 1 <= j by A2, A5, FINSEQ_1:1;

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 A6, FINSEQ_1:59, XXREAL_0:2;

A9: dom m = Seg (len m) by FINSEQ_1:def 3;

then A10: 1 <= i by A1, FINSEQ_1:1;

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 A1, A9, FINSEQ_1:1;

ex l being Element of NAT st

( l in dom f & f . l = m . i )

proof
end;

then consider l being Element of NAT such that per cases
( i < j or i > j )
by A3, XXREAL_0:1;

end;

suppose A12:
i < j
; :: thesis: ex l being Element of NAT st

( l in dom f & f . l = m . i )

( 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 A8, FINSEQ_1:def 3;

then (m | kj) . i = m . i by FUNCT_1:47;

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;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:47;

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

suppose A15:
i > j
; :: thesis: ex l being Element of NAT st

( l in dom f & f . l = m . i )

( 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 A15, XREAL_1:9;

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 A6, RFINSEQ:def 1;

then len f = kj + ((len m) - j) by A8, FINSEQ_1:22

.= (len m) - 1 ;

then A18: ki <= len f by A11, XREAL_1:9;

i - j <= (len m) - j by A11, XREAL_1:9;

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;

reconsider D = INT as set ;

reconsider ww = m9 as FinSequence of D ;

len (m | kj) < i - 1 by A8, A15, XREAL_1:9;

then f . ki = (m /^ j) . (ki - kj) by A8, A18, FINSEQ_1:24

.= (ww /^ j) /. (ki - kj) by A19, PARTFUN1:def 6

.= ww /. (j + a) by A19, FINSEQ_5:27

.= m . i by A1, PARTFUN1:def 6 ;

hence ex l being Element of NAT st

( l in dom f & f . l = m . i ) by A20; :: thesis: verum

end;then reconsider a = (i - 1) - kj as Element of NAT by INT_1:5;

i - kj > (kj + 1) - kj by A15, XREAL_1:9;

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 A6, RFINSEQ:def 1;

then len f = kj + ((len m) - j) by A8, FINSEQ_1:22

.= (len m) - 1 ;

then A18: ki <= len f by A11, XREAL_1:9;

i - j <= (len m) - j by A11, XREAL_1:9;

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;

reconsider D = INT as set ;

reconsider ww = m9 as FinSequence of D ;

len (m | kj) < i - 1 by A8, A15, XREAL_1:9;

then f . ki = (m /^ j) . (ki - kj) by A8, A18, FINSEQ_1:24

.= (ww /^ j) /. (ki - kj) by A19, PARTFUN1:def 6

.= ww /. (j + a) by A19, FINSEQ_5:27

.= m . i by A1, PARTFUN1:def 6 ;

hence ex l being Element of NAT st

( l in dom f & f . l = m . i ) by A20; :: thesis: verum

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:1;

then reconsider kl = l - 1 as Element of NAT by INT_1:5;

l in Seg (len f) by A21, FINSEQ_1:def 3;

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 A2, A5, FINSEQ_1:1;

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 A24, RVSUM_1:97

.= ((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)

.= (Product f) * (m . j) by RVSUM_1:97 ;

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