let n be Element of NAT ; :: thesis: for R1, R2 being Element of n -tuples_on REAL
for r1, r2 being Real holds mlt (R1 ^ <*r1*>),(R2 ^ <*r2*>) = (mlt R1,R2) ^ <*(r1 * r2)*>
let R1, R2 be Element of n -tuples_on REAL ; :: thesis: for r1, r2 being Real holds mlt (R1 ^ <*r1*>),(R2 ^ <*r2*>) = (mlt R1,R2) ^ <*(r1 * r2)*>
let r1, r2 be Real; :: thesis: mlt (R1 ^ <*r1*>),(R2 ^ <*r2*>) = (mlt R1,R2) ^ <*(r1 * r2)*>
len (mlt R1,R2) = n by FINSEQ_1:def 18;
then len ((mlt R1,R2) ^ <*(r1 * r2)*>) = n + 1 by FINSEQ_2:19;
then A1: (mlt R1,R2) ^ <*(r1 * r2)*> is Element of (n + 1) -tuples_on REAL by FINSEQ_2:110;
len (R1 ^ <*r1*>) = (len R1) + 1 by FINSEQ_2:19
.= n + 1 by FINSEQ_1:def 18
.= (len R2) + 1 by FINSEQ_1:def 18
.= len (R2 ^ <*r2*>) by FINSEQ_2:19 ;
then A2: len (mlt (R1 ^ <*r1*>),(R2 ^ <*r2*>)) = len (R1 ^ <*r1*>) by FINSEQ_2:86
.= (len R1) + 1 by FINSEQ_2:19
.= n + 1 by FINSEQ_1:def 18 ;
A3: for k being Nat st k in Seg (n + 1) holds
(mlt (R1 ^ <*r1*>),(R2 ^ <*r2*>)) . k = ((mlt R1,R2) ^ <*(r1 * r2)*>) . k

proof

let k be Nat; :: thesis: ( k in Seg (n + 1) implies (mlt (R1 ^ <*r1*>),(R2 ^ <*r2*>)) . k = ((mlt R1,R2) ^ <*(r1 * r2)*>) . k )
assume A4: k in Seg (n + 1) ; :: thesis: (mlt (R1 ^ <*r1*>),(R2 ^ <*r2*>)) . k = ((mlt R1,R2) ^ <*(r1 * r2)*>) . k
A5: k <= n + 1 by A4, FINSEQ_1:3;

now

per cases ( k < n + 1 or k = n + 1 ) by A5, XXREAL_0:1;

suppose k < n + 1 ; :: thesis: (mlt (R1 ^ <*r1*>),(R2 ^ <*r2*>)) . k = ((mlt R1,R2) ^ <*(r1 * r2)*>) . k

then A6: k <= n by NAT_1:13;
1 <= k by A4, FINSEQ_1:3;
then A7: k in Seg n by A6, FINSEQ_1:3;
then k in Seg (len R1) by FINSEQ_1:def 18;
then k in dom R1 by FINSEQ_1:def 3;
then A8: (R1 ^ <*r1*>) . k = R1 . k by FINSEQ_1:def 7;
k in Seg (len R2) by A7, FINSEQ_1:def 18;
then k in dom R2 by FINSEQ_1:def 3;
then A9: (R2 ^ <*r2*>) . k = R2 . k by FINSEQ_1:def 7;
k in dom (mlt (R1 ^ <*r1*>),(R2 ^ <*r2*>)) by A2, A4, FINSEQ_1:def 3;
then A10: (mlt (R1 ^ <*r1*>),(R2 ^ <*r2*>)) . k = (R1 . k) * (R2 . k) by A8, A9, RVSUM_1:86;
len (mlt R1,R2) = n by FINSEQ_1:def 18;
then A11: k in dom (mlt R1,R2) by A7, FINSEQ_1:def 3;
then ((mlt R1,R2) ^ <*(r1 * r2)*>) . k = (mlt R1,R2) . k by FINSEQ_1:def 7;
hence (mlt (R1 ^ <*r1*>),(R2 ^ <*r2*>)) . k = ((mlt R1,R2) ^ <*(r1 * r2)*>) . k by A10, A11, RVSUM_1:86; :: thesis: verum

end;

suppose A12: k = n + 1 ; :: thesis: (mlt (R1 ^ <*r1*>),(R2 ^ <*r2*>)) . k = ((mlt R1,R2) ^ <*(r1 * r2)*>) . k

then k = (len R1) + 1 by FINSEQ_1:def 18;
then A13: (R1 ^ <*r1*>) . k = r1 by FINSEQ_1:59;
A14: n + 1 = (len (mlt R1,R2)) + 1 by FINSEQ_1:def 18;
k = (len R2) + 1 by A12, FINSEQ_1:def 18;
then A15: (R2 ^ <*r2*>) . k = r2 by FINSEQ_1:59;
k in dom (mlt (R1 ^ <*r1*>),(R2 ^ <*r2*>)) by A2, A4, FINSEQ_1:def 3;
then (mlt (R1 ^ <*r1*>),(R2 ^ <*r2*>)) . k = r1 * r2 by A13, A15, RVSUM_1:86;
hence (mlt (R1 ^ <*r1*>),(R2 ^ <*r2*>)) . k = ((mlt R1,R2) ^ <*(r1 * r2)*>) . k by A12, A14, FINSEQ_1:59; :: thesis: verum

end;

end;

end;

hence (mlt (R1 ^ <*r1*>),(R2 ^ <*r2*>)) . k = ((mlt R1,R2) ^ <*(r1 * r2)*>) . k ; :: thesis: verum

end;

mlt (R1 ^ <*r1*>),(R2 ^ <*r2*>) is Element of (n + 1) -tuples_on REAL by A2, FINSEQ_2:110;
hence mlt (R1 ^ <*r1*>),(R2 ^ <*r2*>) = (mlt R1,R2) ^ <*(r1 * r2)*> by A1, A3, FINSEQ_2:139; :: thesis: verum