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 FINSEQ_1:def 18;
A2: len (n |-> 0 ) = n by FINSEQ_1:def 18;
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 A3: ( 1 <= k & k <= len (mlt (n |-> 0 ),R) ) ; :: thesis: (mlt (n |-> 0 ),R) . k = (n |-> 0 ) . k
A4: k in Seg (len (mlt (n |-> 0 ),R)) by A3, FINSEQ_1:3;
(mlt (n |-> 0 ),R) . k = ((n |-> 0 ) . k) * (R . k) by RVSUM_1:87
.= 0 * (R . k) by A1, A4, FUNCOP_1:13 ;
hence (mlt (n |-> 0 ),R) . k = (n |-> 0 ) . k by A1, A4, FUNCOP_1:13; :: thesis: verum

end;

hence mlt (n |-> 0 ),R = n |-> 0 by A1, A2, FINSEQ_1:18; :: thesis: verum