let n be 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)*>
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; :: 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: k <= n + 1 by A3, FINSEQ_1:1;
now :: thesis: (mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>))) . k = ((mlt (R1,R2)) ^ <*(r1 * r2)*>) . k
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 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; :: 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 by CARD_1:def 7;
then A10: (R1 ^ <*r1*>) . k = r1 by FINSEQ_1:42;
A11: n + 1 = (len (mlt (R1,R2))) + 1 by CARD_1:def 7;
k = (len R2) + 1 by A9, CARD_1:def 7;
then (R2 ^ <*r2*>) . k = r2 by FINSEQ_1:42;
then (mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>))) . k = r1 * r2 by A10, RVSUM_1:59;
hence (mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>))) . k = ((mlt (R1,R2)) ^ <*(r1 * r2)*>) . k by A9, A11, FINSEQ_1:42; :: thesis: verum
end;
end;
end;
hence (mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>))) . k = ((mlt (R1,R2)) ^ <*(r1 * r2)*>) . k ; :: thesis: 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; :: thesis: verum