let F1, F2 be FinSequence of COMPLEX ; :: thesis: for i being Nat st i in dom (mlt (F1,F2)) holds
(mlt (F1,F2)) . i = (F1 . i) * (F2 . i)
let i be Nat; :: thesis: ( i in dom (mlt (F1,F2)) implies (mlt (F1,F2)) . i = (F1 . i) * (F2 . i) )
set r1 = F1 . i;
set r2 = F2 . i;
assume i in dom (mlt (F1,F2)) ; :: thesis: (mlt (F1,F2)) . i = (F1 . i) * (F2 . i)
then (mlt (F1,F2)) . i = multcomplex . ((F1 . i),(F2 . i)) by FUNCOP_1:22;
hence (mlt (F1,F2)) . i = (F1 . i) * (F2 . i) by BINOP_2:def 5; :: thesis: verum