let m be integer-valued FinSequence; :: thesis: for i being Nat holds (Product m) / (m . i) is Integer
let i be Nat; :: thesis: (Product m) / (m . i) is Integer
reconsider m2 = m /^ i as FinSequence of INT ;
reconsider m1 = m | i as FinSequence of INT by FINSEQ_1:102;
reconsider m9 = m as FinSequence of INT by FINSEQ_1:102;

per cases ( not i in dom m or m . i = 0 or ( i in dom m & m . i <> 0 ) ) ;

suppose ( not i in dom m or m . i = 0 ) ; :: thesis: (Product m) / (m . i) is Integer

then m . i = 0 by FUNCT_1:def 2;
hence (Product m) / (m . i) is Integer ; :: thesis: verum

end;

suppose that A1: i in dom m and
A2: m . i <> 0 ; :: thesis: (Product m) / (m . i) is Integer

A3: dom m = Seg (len m) by FINSEQ_1:def 3;
then 1 <= i by A1, FINSEQ_1:1;
then reconsider j = i - 1 as Element of NAT by INT_1:3;
set f = (m | j) ^ (m /^ i);
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 ((m | j) ^ (m /^ i))) * (m . i) by RVSUM_1:97 ;
then m . i divides Product m by INT_1:def 3;
hence (Product m) / (m . i) is Integer by A2, WSIERP_1:17; :: thesis: verum

end;

end;