let n be Element of NAT ; :: thesis: for R being Element of n -tuples_on REAL holds mlt ((n |-> 0),R) = n |-> 0
let R be Element of n -tuples_on REAL; :: thesis: mlt ((n |-> 0),R) = n |-> 0
A1: len (mlt ((n |-> 0),R)) = n by CARD_1:def 7;
A2: for k being Nat st 1 <= k & k <= len (mlt ((n |-> 0),R)) holds
(mlt ((n |-> 0),R)) . k = (n |-> 0) . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len (mlt ((n |-> 0),R)) implies (mlt ((n |-> 0),R)) . k = (n |-> 0) . k )
assume ( 1 <= k & k <= len (mlt ((n |-> 0),R)) ) ; :: thesis: (mlt ((n |-> 0),R)) . k = (n |-> 0) . k
then A3: k in Seg (len (mlt ((n |-> 0),R))) by FINSEQ_1:1;
(mlt ((n |-> 0),R)) . k = ((n |-> 0) . k) * (R . k) by RVSUM_1:60
.= 0 * (R . k) by A1, A3, FUNCOP_1:7 ;
hence (mlt ((n |-> 0),R)) . k = (n |-> 0) . k by A1, A3, FUNCOP_1:7; :: thesis: verum

end;

len (n |-> 0) = n by CARD_1:def 7;
hence mlt ((n |-> 0),R) = n |-> 0 by A1, A2, FINSEQ_1:14; :: thesis: verum