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 that
A1: len e1 = len e2 and
A2: e1 = f1 and
A3: e2 = f2 ; :: thesis: 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:110;
mlt e3,e4 = mlt f3,f4 by A2, A3, Th34;
hence mlt e1,e2 = mlt f1,f2 ; :: thesis: verum