let f1, f2 be FinSequence of REAL ; ( len f1 = 3 & len f2 = 3 implies mlt (f1,f2) = <*((f1 . 1) * (f2 . 1)),((f1 . 2) * (f2 . 2)),((f1 . 3) * (f2 . 3))*> )
assume that
A1:
len f1 = 3
and
A2:
len f2 = 3
; mlt (f1,f2) = <*((f1 . 1) * (f2 . 1)),((f1 . 2) * (f2 . 2)),((f1 . 3) * (f2 . 3))*>
A3:
f2 = <*(f2 . 1),(f2 . 2),(f2 . 3)*>
by A2, FINSEQ_1:45;
reconsider f11 = f1 . 1, f12 = f1 . 2, f13 = f1 . 3, f21 = f2 . 1, f22 = f2 . 2, f23 = f2 . 3 as Element of REAL by XREAL_0:def 1;
mlt (f1,f2) =
multreal .: (f1,f2)
by RVSUM_1:def 9
.=
multreal .: (<*f11,f12,f13*>,<*f21,f22,f23*>)
by A1, A3, FINSEQ_1:45
.=
<*(multreal . ((f1 . 1),(f2 . 1))),(multreal . ((f1 . 2),(f2 . 2))),(multreal . ((f1 . 3),(f2 . 3)))*>
by FINSEQ_2:76
.=
<*((f1 . 1) * (f2 . 1)),(multreal . ((f1 . 2),(f2 . 2))),(multreal . ((f1 . 3),(f2 . 3)))*>
by BINOP_2:def 11
.=
<*((f1 . 1) * (f2 . 1)),((f1 . 2) * (f2 . 2)),(multreal . ((f1 . 3),(f2 . 3)))*>
by BINOP_2:def 11
;
hence
mlt (f1,f2) = <*((f1 . 1) * (f2 . 1)),((f1 . 2) * (f2 . 2)),((f1 . 3) * (f2 . 3))*>
by BINOP_2:def 11; verum