let m be INT -valued FinSequence; :: thesis: for i, j being Nat st i <> j holds
(Product m) / ((m . i) * (m . j)) is Integer
let i9, j9 be Nat; :: thesis: ( i9 <> j9 implies (Product m) / ((m . i9) * (m . j9)) is Integer )
assume A3: j9 <> i9 ; :: thesis: (Product m) / ((m . i9) * (m . j9)) is Integer

per cases ( i9 in dom m or not i9 in dom m ) ;

suppose A1: i9 in dom m ; :: thesis: (Product m) / ((m . i9) * (m . j9)) is Integer

reconsider i = i9, j = j9 as Element of NAT by ORDINAL1:def 12;
A5: ex z being Integer st z * (m . i) = (Product m) / (m . j) by A1, A3, 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 ;
A7: u / (m . i) = (Product m) * (((m . j) ") * ((m . i) "))
.= (Product m) / ((m . i) * (m . j)) by XCMPLX_1:204 ;
m . i divides u by A5, INT_1:def 3;
hence (Product m) / ((m . i9) * (m . j9)) is Integer by A6, A7, WSIERP_1:17; :: thesis: verum

end;

end;

end;

suppose not i9 in dom m ; :: thesis: (Product m) / ((m . i9) * (m . j9)) is Integer

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

end;

end;