let f1, f2 be FinSequence of REAL ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum