let m be integer-yielding FinSequence; :: thesis: for i, j being natural number st i in dom m & j in dom m & j <> i & m . j <> 0 holds
(Product m) / ((m . i) * (m . j)) is Integer
let i', j' be natural number ; :: thesis: ( i' in dom m & j' in dom m & j' <> i' & m . j' <> 0 implies (Product m) / ((m . i') * (m . j')) is Integer )
assume AS: ( i' in dom m & j' in dom m & j' <> i' & m . j' <> 0 ) ; :: thesis: (Product m) / ((m . i') * (m . j')) is Integer
reconsider i = i', j = j' as Element of NAT by ORDINAL1:def 13;
consider z being Integer such that
H: z * (m . i) = (Product m) / (m . j) by AS, x0000;

per cases ( m . i = 0 or m . i <> 0 ) ;

suppose m . i = 0 ; :: thesis: (Product m) / ((m . i') * (m . j')) is Integer

then 0 = Product m by AS, mtriv;
hence (Product m) / ((m . i') * (m . j')) is Integer ; :: thesis: verum

end;

suppose A: m . i <> 0 ; :: thesis: (Product m) / ((m . i') * (m . j')) is Integer

reconsider u = (Product m) / (m . j) as Integer by AS, prodint;
B: m . i divides u by H, INT_1:def 9;
u / (m . i) = (Product m) * (((m . j) " ) * ((m . i) " ))
.= (Product m) / ((m . i) * (m . j)) by XCMPLX_1:205 ;
hence (Product m) / ((m . i') * (m . j')) is Integer by A, B, WSIERP_1:22; :: thesis: verum

end;

end;