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
mlt e1,e2 = mlt f1,f2
let f1, f2 be FinSequence of F_Real ; :: thesis: ( len e1 = len e2 & e1 = f1 & e2 = f2 implies mlt e1,e2 = mlt f1,f2 )
assume A1: ( len e1 = len e2 & e1 = f1 & e2 = f2 ) ; :: thesis: mlt e1,e2 = mlt f1,f2
set l = len e1;
set Y = { e where e is Element of REAL * : len e = len e1 } ;
set Z = { f where f is Element of the carrier of F_Real * : len f = len e1 } ;
reconsider e3 = e1 as Element of (len e1) -tuples_on REAL by FINSEQ_2:110;
( len e2 = len e1 & e2 is Element of REAL * ) by A1, FINSEQ_1:def 11;
then e2 in { e where e is Element of REAL * : len e = len e1 } ;
then reconsider e4 = e2 as Element of (len e1) -tuples_on REAL ;
( len f1 = len e1 & f1 is Element of the carrier of F_Real * ) by A1, FINSEQ_1:def 11;
then f1 in { f where f is Element of the carrier of F_Real * : len f = len e1 } ;
then reconsider f3 = f1 as Element of (len e1) -tuples_on the carrier of F_Real ;
( len f2 = len e1 & f2 is Element of the carrier of F_Real * ) by A1, FINSEQ_1:def 11;
then f2 in { f where f is Element of the carrier of F_Real * : len f = len e1 } ;
then reconsider f4 = f2 as Element of (len e1) -tuples_on the carrier of F_Real ;
mlt e3,e4 = mlt f3,f4 by A1, Th34;
hence mlt e1,e2 = mlt f1,f2 ; :: thesis: verum