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:92;
mlt (e3,e4) = mlt (f3,f4) by A2, A3, Th34;
hence mlt (e1,e2) = mlt (f1,f2) ; :: thesis: verum