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:62;
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:62
.= <*(multreal . (f1 . 1),(f2 . 1)),(multreal . (f1 . 2),(f2 . 2)),(multreal . (f1 . 3),(f2 . 3))*> by FINSEQ_2:90
.= <*((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