let m be integer-yielding FinSequence; :: thesis: for i being natural number st i in dom m holds
ex z being Integer st z * (m . i) = Product m
let i be natural number ; :: thesis: ( i in dom m implies ex z being Integer st z * (m . i) = Product m )
assume AS: i in dom m ; :: thesis: ex z being Integer st z * (m . i) = Product m

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

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

then reconsider z = (Product m) / (m . i) as Integer by AS, prodint;
take z ; :: thesis: z * (m . i) = Product m
thus z * (m . i) = (Product m) * (((m . i) " ) * (m . i))
.= (Product m) * 1 by C, XCMPLX_0:def 7
.= Product m ; :: thesis: verum

end;

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

take 1 ; :: thesis: 1 * (m . i) = Product m
thus 1 * (m . i) = Product m by C, AS, mtriv; :: thesis: verum

end;

end;