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