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:28;
hence (mlt F1,F2) . i = (F1 . i) * (F2 . i) by BINOP_2:def 5; :: thesis: verum