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
mlt (e1,e2) = mlt (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
mlt (e1,e2) = mlt (f1,f2)
let f1, f2 be Element of i -tuples_on the carrier of F_Real; :: thesis: ( e1 = f1 & e2 = f2 implies mlt (e1,e2) = mlt (f1,f2) )
assume A1: ( e1 = f1 & e2 = f2 ) ; :: thesis: mlt (e1,e2) = mlt (f1,f2)
A2: dom (mlt (e1,e2)) = Seg (len (mlt (e1,e2))) by FINSEQ_1:def 3
.= Seg i by CARD_1:def 7
.= Seg (len (mlt (f1,f2))) by CARD_1:def 7
.= dom (mlt (f1,f2)) by FINSEQ_1:def 3 ;
for i being Nat st i in dom (mlt (e1,e2)) holds
(mlt (e1,e2)) . i = (mlt (f1,f2)) . i

proof

let i be Nat; :: thesis: ( i in dom (mlt (e1,e2)) implies (mlt (e1,e2)) . i = (mlt (f1,f2)) . i )
assume A3: i in dom (mlt (e1,e2)) ; :: thesis: (mlt (e1,e2)) . i = (mlt (f1,f2)) . i
( e1 . i in REAL & e2 . i in REAL ) by XREAL_0:def 1;
then reconsider a1 = e1 . i, a2 = e2 . i as Element of F_Real by VECTSP_1:def 5;
thus (mlt (e1,e2)) . i = a1 * a2 by RVSUM_1:59
.= (mlt (f1,f2)) . i by A1, A2, A3, FVSUM_1:60 ; :: thesis: verum

end;

hence mlt (e1,e2) = mlt (f1,f2) by A2, FINSEQ_1:13; :: thesis: verum