let n be Nat; 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; for r1, r2 being Real holds mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>)) = (mlt (R1,R2)) ^ <*(r1 * r2)*>
let r1, r2 be Real; mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>)) = (mlt (R1,R2)) ^ <*(r1 * r2)*>
reconsider r1 = r1, r2 = r2 as Element of REAL by XREAL_0:def 1;
len (R1 ^ <*r1*>) =
(len R1) + 1
by FINSEQ_2:16
.=
n + 1
by CARD_1:def 7
.=
(len R2) + 1
by CARD_1:def 7
.=
len (R2 ^ <*r2*>)
by FINSEQ_2:16
;
then A1: len (mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>))) =
len (R1 ^ <*r1*>)
by FINSEQ_2:72
.=
(len R1) + 1
by FINSEQ_2:16
.=
n + 1
by CARD_1:def 7
;
A2:
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;
( 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)
;
(mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>))) . k = ((mlt (R1,R2)) ^ <*(r1 * r2)*>) . k
A4:
k <= n + 1
by A3, FINSEQ_1:1;
now (mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>))) . k = ((mlt (R1,R2)) ^ <*(r1 * r2)*>) . kper cases
( k < n + 1 or k = n + 1 )
by A4, XXREAL_0:1;
suppose
k < n + 1
;
(mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>))) . k = ((mlt (R1,R2)) ^ <*(r1 * r2)*>) . kthen A5:
k <= n
by NAT_1:13;
1
<= k
by A3, FINSEQ_1:1;
then A6:
k in Seg n
by A5, FINSEQ_1:1;
then
k in Seg (len R1)
by CARD_1:def 7;
then
k in dom R1
by FINSEQ_1:def 3;
then A7:
(R1 ^ <*r1*>) . k = R1 . k
by FINSEQ_1:def 7;
k in Seg (len R2)
by A6, CARD_1:def 7;
then
k in dom R2
by FINSEQ_1:def 3;
then
(R2 ^ <*r2*>) . k = R2 . k
by FINSEQ_1:def 7;
then A8:
(mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>))) . k = (R1 . k) * (R2 . k)
by A7, RVSUM_1:59;
len (mlt (R1,R2)) = n
by CARD_1:def 7;
then
k in dom (mlt (R1,R2))
by A6, 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 A8, RVSUM_1:59;
verum end; end; end;
hence
(mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>))) . k = ((mlt (R1,R2)) ^ <*(r1 * r2)*>) . k
;
verum
end;
reconsider rr = r1 * r2 as Element of REAL ;
mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>)) is Element of (n + 1) -tuples_on REAL
by A1, FINSEQ_2:92;
hence
mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>)) = (mlt (R1,R2)) ^ <*(r1 * r2)*>
by A2, FINSEQ_2:119; verum