let e1, e2 be FinSequence of REAL ; :: thesis: for f1, f2 being FinSequence of F_Real st len e1 = len e2 & e1 = f1 & e2 = f2 holds
e1 "*" e2 = f1 "*" f2
let f1, f2 be FinSequence of F_Real; :: thesis: ( len e1 = len e2 & e1 = f1 & e2 = f2 implies e1 "*" e2 = f1 "*" f2 )
assume ( len e1 = len e2 & e1 = f1 & e2 = f2 ) ; :: thesis: e1 "*" e2 = f1 "*" f2
hence e1 "*" e2 = Sum (mlt (f1,f2)) by Th35, Th36
.= f1 "*" f2 by FVSUM_1:def 9 ;
:: thesis: verum