let i be Nat; :: thesis: for c1, c2 being complex number holds mlt (i |-> c1),(i |-> c2) = i |-> (c1 * c2)
let c1, c2 be complex number ; :: thesis: mlt (i |-> c1),(i |-> c2) = i |-> (c1 * c2)
reconsider s1 = c1, s2 = c2 as Element of COMPLEX by XCMPLX_0:def 2;
mlt (i |-> s1),(i |-> s2) = s1 * (i |-> s2) by Th92
.= i |-> (c1 * c2) by Th70 ;
hence mlt (i |-> c1),(i |-> c2) = i |-> (c1 * c2) ; :: thesis: verum