let n be 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 |-> (In (0,REAL))),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
(mlt ((n |-> 0),R)) . k = ((n |-> 0) . k) * (R . k) by RVSUM_1:60
.= 0 * (R . k) ;
hence (mlt ((n |-> 0),R)) . k = (n |-> 0) . k ; :: 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