let i be Nat; :: thesis: for e1, e2 being Element of i -tuples_on REAL
for f1, f2 being Element of i -tuples_on the carrier of F_Real st e1 = f1 & e2 = f2 holds
e1 "*" e2 = f1 "*" f2
let e1, e2 be Element of i -tuples_on REAL; :: thesis: for f1, f2 being Element of i -tuples_on the carrier of F_Real st e1 = f1 & e2 = f2 holds
e1 "*" e2 = f1 "*" f2
let f1, f2 be Element of i -tuples_on the carrier of F_Real; :: thesis: ( e1 = f1 & e2 = f2 implies e1 "*" e2 = f1 "*" f2 )
assume ( e1 = f1 & e2 = f2 ) ; :: thesis: e1 "*" e2 = f1 "*" f2
hence e1 "*" e2 = Sum (mlt (f1,f2)) by Th34, Th36
.= f1 "*" f2 by FVSUM_1:def 9 ;
:: thesis: verum