let m be integer-yielding FinSequence; :: thesis: for i being natural number st i in dom m & m . i <> 0 holds
(Product m) / (m . i) is Integer
let i' be natural number ; :: thesis: ( i' in dom m & m . i' <> 0 implies (Product m) / (m . i') is Integer )
assume AS: ( i' in dom m & m . i' <> 0 ) ; :: thesis: (Product m) / (m . i') is Integer
reconsider i = i' as Element of NAT by ORDINAL1:def 13;
A3: dom m = Seg (len m) by FINSEQ_1:def 3;
then ( 1 <= i & i <= len m ) by AS, FINSEQ_1:3;
then 1 - 1 <= i - 1 by XREAL_1:11;
then reconsider j = i - 1 as Element of NAT by INT_1:16;
set f = (m | j) ^ (m /^ i);
j + 1 <= len m by A3, AS, FINSEQ_1:3;
then A4: (m | j) ^ <*(m . i)*> = m | i by th67;
reconsider m' = m as FinSequence of INT by intint;
reconsider m1 = m | i as FinSequence of INT by intint;
reconsider m2 = m /^ i as FinSequence of INT by intint;
reconsider f = (m | j) ^ (m /^ i) as FinSequence of INT by intint;
m' = m1 ^ m2 by RFINSEQ:21;
then Product m = (Product ((m | j) ^ <*(m . i)*>)) * (Product (m /^ i)) by A4, RVSUM_1:127
.= ((Product (m | j)) * (Product <*(m . i)*>)) * (Product (m /^ i)) by RVSUM_1:127
.= ((Product (m | j)) * (Product (m /^ i))) * (Product <*(m . i)*>)
.= ((Product (m | j)) * (Product (m /^ i))) * (m . i) by RVSUM_1:125
.= (Product f) * (m . i) by RVSUM_1:127 ;
then m . i divides Product m by INT_1:def 9;
hence (Product m) / (m . i') is Integer by AS, WSIERP_1:22; :: thesis: verum