let m be INT -valued FinSequence; :: thesis: for i, j being Nat 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 Nat; :: 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 12;

A5: ex z being Integer st z * (m . i) = (Product m) / (m . j) by A1, A2, A3, A4, Lm6;

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

let i9, j9 be Nat; :: 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 12;

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 )
;

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: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;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