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)*>
A1: mlt (R1 ^ <*r1*>),(R2 ^ <*r2*>) is Element of (n + 1) -tuples_on REAL

proof

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 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 ;
hence mlt (R1 ^ <*r1*>),(R2 ^ <*r2*>) is Element of (n + 1) -tuples_on REAL by FINSEQ_2:110; :: thesis: verum

end;

A2: (mlt R1,R2) ^ <*(r1 * r2)*> is Element of (n + 1) -tuples_on REAL

proof

len (mlt R1,R2) = n by FINSEQ_1:def 18;
then len ((mlt R1,R2) ^ <*(r1 * r2)*>) = n + 1 by FINSEQ_2:19;
hence (mlt R1,R2) ^ <*(r1 * r2)*> is Element of (n + 1) -tuples_on REAL by FINSEQ_2:110; :: thesis: verum

end;

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 A3: k in Seg (n + 1) ; :: thesis: (mlt (R1 ^ <*r1*>),(R2 ^ <*r2*>)) . k = ((mlt R1,R2) ^ <*(r1 * r2)*>) . k
A4: ( 1 <= k & k <= n + 1 ) by A3, FINSEQ_1:3;

now

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

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

then ( 1 <= k & k <= n ) by A3, FINSEQ_1:3, NAT_1:13;
then A5: k in Seg n by FINSEQ_1:3;
then ( k in Seg (len R1) & k in Seg (len R2) ) by FINSEQ_1:def 18;
then ( k in dom R1 & k in dom R2 ) by FINSEQ_1:def 3;
then A6: ( (R1 ^ <*r1*>) . k = R1 . k & (R2 ^ <*r2*>) . k = R2 . k ) by FINSEQ_1:def 7;
k in Seg (len (mlt (R1 ^ <*r1*>),(R2 ^ <*r2*>))) by A1, A3, FINSEQ_1:def 18;
then k in dom (mlt (R1 ^ <*r1*>),(R2 ^ <*r2*>)) by FINSEQ_1:def 3;
then A7: (mlt (R1 ^ <*r1*>),(R2 ^ <*r2*>)) . k = (R1 . k) * (R2 . k) by A6, RVSUM_1:86;
len (mlt R1,R2) = n by FINSEQ_1:def 18;
then A8: k in dom (mlt R1,R2) by A5, 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 A7, A8, RVSUM_1:86; :: thesis: verum

end;

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

then ( k = (len R1) + 1 & k = (len R2) + 1 ) by FINSEQ_1:def 18;
then A10: ( (R1 ^ <*r1*>) . k = r1 & (R2 ^ <*r2*>) . k = r2 ) by FINSEQ_1:59;
k in Seg (len (mlt (R1 ^ <*r1*>),(R2 ^ <*r2*>))) by A1, A3, FINSEQ_1:def 18;
then k in dom (mlt (R1 ^ <*r1*>),(R2 ^ <*r2*>)) by FINSEQ_1:def 3;
then A11: (mlt (R1 ^ <*r1*>),(R2 ^ <*r2*>)) . k = r1 * r2 by A10, RVSUM_1:86;
n + 1 = (len (mlt R1,R2)) + 1 by FINSEQ_1:def 18;
hence (mlt (R1 ^ <*r1*>),(R2 ^ <*r2*>)) . k = ((mlt R1,R2) ^ <*(r1 * r2)*>) . k by A9, A11, FINSEQ_1:59; :: thesis: verum

end;

end;

end;

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

end;

hence mlt (R1 ^ <*r1*>),(R2 ^ <*r2*>) = (mlt R1,R2) ^ <*(r1 * r2)*> by A1, A2, FINSEQ_2:139; :: thesis: verum