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
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 (0* n) = n by FINSEQ_1:def 18;
then A2: dom (0* n) = Seg n by FINSEQ_1:def 3;
A3: 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 A4: j in dom (0* n) ; :: thesis: (mlt v,(0* n)) . j = (0* n) . j
thus (mlt v,(0* n)) . j = 0 by Th1
.= (n |-> 0 ) . j by A2, A4, FUNCOP_1:13
.= (0* n) . j by EUCLID:def 4 ; :: thesis: verum

end;

len (mlt v,z) = n by FINSEQ_1:def 18;
then dom (mlt v,(0* n)) = dom (0* n) by A1, FINSEQ_3:31;
hence mlt v,(0* n) = 0* n by A3, FINSEQ_1:17; :: thesis: verum