let m be INT -valued FinSequence; :: thesis: for i being Nat st i in dom m & m . i <> 0 holds

(Product m) / (m . i) is Integer

let i9 be Nat; :: 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)

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

(Product m) / (m . i) is Integer

let i9 be Nat; :: 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)

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