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

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

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

reconsider rr = r1 * r2 as Element of REAL ;
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;

end;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)*>) . kend;

hence
(mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>))) . k = ((mlt (R1,R2)) ^ <*(r1 * r2)*>) . k
; :: thesis: verumper cases
( k < n + 1 or k = n + 1 )
by A4, XXREAL_0:1;

end;

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;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

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;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

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