let n be Nat; :: thesis: for v being Element of n -tuples_on REAL holds mlt v,(0* n) = 0* n
let v be Element of n -tuples_on REAL ; :: thesis: mlt v,(0* n) = 0* n
0* n = n |-> 0 by EUCLID:def 4;
then len (0* n) = n by FINSEQ_1:def 18;
then reconsider z = 0* n as Element of n -tuples_on REAL by FINSEQ_2:110;
A1: len (mlt v,z) = n by FINSEQ_1:def 18;
0* n = n |-> 0 by EUCLID:def 4;
then A2: len (0* n) = n by FINSEQ_1:def 18;
then A3: dom (mlt v,(0* n)) = dom (0* n) by A1, FINSEQ_3:31;
A4: dom (0* n) = Seg n by A2, FINSEQ_1:def 3;
for j being Nat st j in dom (0* n) holds
(mlt v,(0* n)) . j = (0* n) . j

proof

let j be Nat; :: thesis: ( j in dom (0* n) implies (mlt v,(0* n)) . j = (0* n) . j )
assume A5: j in dom (0* n) ; :: thesis: (mlt v,(0* n)) . j = (0* n) . j
hence (mlt v,(0* n)) . j = 0 by A4, Th1
.= (n |-> 0 ) . j by A4, A5, FUNCOP_1:13
.= (0* n) . j by EUCLID:def 4 ;
:: thesis: verum

end;

hence mlt v,(0* n) = 0* n by A3, FINSEQ_1:17; :: thesis: verum