let m be INT -valued FinSequence; :: thesis: for i being Nat st i in dom m holds

ex z being Integer st z * (m . i) = Product m

let i be Nat; :: thesis: ( i in dom m implies ex z being Integer st z * (m . i) = Product m )

assume A1: i in dom m ; :: thesis: ex z being Integer st z * (m . i) = Product m

ex z being Integer st z * (m . i) = Product m

let i be Nat; :: thesis: ( i in dom m implies ex z being Integer st z * (m . i) = Product m )

assume A1: i in dom m ; :: thesis: ex z being Integer st z * (m . i) = Product m

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

end;

suppose A2:
m . i <> 0
; :: thesis: ex z being Integer st z * (m . i) = Product m

then reconsider z = (Product m) / (m . i) as Integer by A1, Th9;

take z ; :: thesis: z * (m . i) = Product m

thus z * (m . i) = (Product m) * (((m . i) ") * (m . i))

.= (Product m) * 1 by A2, XCMPLX_0:def 7

.= Product m ; :: thesis: verum

end;take z ; :: thesis: z * (m . i) = Product m

thus z * (m . i) = (Product m) * (((m . i) ") * (m . i))

.= (Product m) * 1 by A2, XCMPLX_0:def 7

.= Product m ; :: thesis: verum