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 i9 be natural number ; :: thesis: ( i9 in dom m & m . i9 <> 0 implies (Product m) / (m . i9) is Integer )
reconsider i = i9 as Element of NAT by ORDINAL1:def 12;
reconsider m2 = m /^ i as FinSequence of INT by Lm1;
reconsider m1 = m | i as FinSequence of INT by Lm1;
reconsider m9 = m as FinSequence of INT by Lm1;
assume that
A1: i9 in dom m and
A2: m . i9 <> 0 ; :: thesis: (Product m) / (m . i9) is Integer
A3: dom m = Seg (len m) by FINSEQ_1:def 3;
then 1 <= i by A1, FINSEQ_1:1;
then 1 - 1 <= i - 1 by XREAL_1:9;
then reconsider j = i - 1 as Element of NAT by INT_1:3;
set f = (m | j) ^ (m /^ i);
reconsider f = (m | j) ^ (m /^ i) as FinSequence of INT by Lm1;
A4: m9 = m1 ^ m2 by RFINSEQ:8;
j + 1 <= len m by A1, A3, FINSEQ_1:1;
then (m | j) ^ <*(m . i)*> = m | i by Th5;
then Product m = (Product ((m | j) ^ <*(m . i)*>)) * (Product (m /^ i)) by A4, RVSUM_1:97
.= ((Product (m | j)) * (Product <*(m . i)*>)) * (Product (m /^ i)) by RVSUM_1:97
.= ((Product (m | j)) * (Product (m /^ i))) * (Product <*(m . i)*>)
.= ((Product (m | j)) * (Product (m /^ i))) * (m . i) by RVSUM_1:95
.= (Product f) * (m . i) by RVSUM_1:97 ;
then m . i divides Product m by INT_1:def 3;
hence (Product m) / (m . i9) is Integer by A2, WSIERP_1:17; :: thesis: verum