let i be Element of 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 FINSEQ_1:def 18
.= Seg (len (mlt f1,f2)) by FINSEQ_1:def 18
.= 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
reconsider a1 = e1 . i, a2 = e2 . i as Element of F_Real by VECTSP_1:def 15;
thus (mlt e1,e2) . i = a1 * a2 by A3, RVSUM_1:86
.= (mlt f1,f2) . i by A1, A2, A3, FVSUM_1:73 ; :: thesis: verum

end;

hence mlt e1,e2 = mlt f1,f2 by A2, FINSEQ_1:17; :: thesis: verum