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 i9, j9 be natural number ; :: thesis: ( i9 in dom m & j9 in dom m & j9 <> i9 & m . j9 <> 0 implies (Product m) / ((m . i9) * (m . j9)) is Integer )
assume that
A1: i9 in dom m and
A2: j9 in dom m and
A3: j9 <> i9 and
A4: m . j9 <> 0 ; :: thesis: (Product m) / ((m . i9) * (m . j9)) is Integer
reconsider i = i9, j = j9 as Element of NAT by ORDINAL1:def 13;
A5: ex z being Integer st z * (m . i) = (Product m) / (m . j) by A1, A2, A3, A4, Lm6;

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

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

hence (Product m) / ((m . i9) * (m . j9)) is Integer ; :: thesis: verum

end;

suppose A6: m . i <> 0 ; :: thesis: (Product m) / ((m . i9) * (m . j9)) is Integer

reconsider u = (Product m) / (m . j) as Integer by A2, A4, Th9;
A7: u / (m . i) = (Product m) * (((m . j) " ) * ((m . i) " ))
.= (Product m) / ((m . i) * (m . j)) by XCMPLX_1:205 ;
m . i divides u by A5, INT_1:def 9;
hence (Product m) / ((m . i9) * (m . j9)) is Integer by A6, A7, WSIERP_1:22; :: thesis: verum

end;

end;