let e1, e2 be FinSequence of REAL ; for f1, f2 being FinSequence of F_Real st len e1 = len e2 & e1 = f1 & e2 = f2 holds
mlt (e1,e2) = mlt (f1,f2)
let f1, f2 be FinSequence of F_Real; ( len e1 = len e2 & e1 = f1 & e2 = f2 implies mlt (e1,e2) = mlt (f1,f2) )
assume that
A1:
len e1 = len e2
and
A2:
e1 = f1
and
A3:
e2 = f2
; mlt (e1,e2) = mlt (f1,f2)
set l = len e1;
set Z = { f where f is Element of the carrier of F_Real * : len f = len e1 } ;
f1 is Element of the carrier of F_Real *
by FINSEQ_1:def 11;
then
f1 in { f where f is Element of the carrier of F_Real * : len f = len e1 }
by A2;
then reconsider f3 = f1 as Element of (len e1) -tuples_on the carrier of F_Real ;
f2 is Element of the carrier of F_Real *
by FINSEQ_1:def 11;
then
f2 in { f where f is Element of the carrier of F_Real * : len f = len e1 }
by A1, A3;
then reconsider f4 = f2 as Element of (len e1) -tuples_on the carrier of F_Real ;
set Y = { e where e is Element of REAL * : len e = len e1 } ;
e2 is Element of REAL *
by FINSEQ_1:def 11;
then
e2 in { e where e is Element of REAL * : len e = len e1 }
by A1;
then reconsider e4 = e2 as Element of (len e1) -tuples_on REAL ;
reconsider e3 = e1 as Element of (len e1) -tuples_on REAL by FINSEQ_2:92;
mlt (e3,e4) = mlt (f3,f4)
by A2, A3, Th34;
hence
mlt (e1,e2) = mlt (f1,f2)
; verum