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;
mlt (f1,f2) = multreal .: (f1,f2) by RVSUM_1:def 9
.= multreal .: (<*(f1 . 1),(f1 . 2),(f1 . 3)*>,<*(f2 . 1),(f2 . 2),(f2 . 3)*>) 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