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

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

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

take z = (Product m) / (m . i); :: 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;

suppose A3: 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 A1, A3, Th6; :: thesis: verum

end;

end;