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 CARD_1:def 7;
then reconsider z = 0* n as Element of n -tuples_on REAL by FINSEQ_2:92;
A1: len (0* n) = n by CARD_1:def 7;
A2: 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 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
.= (0* n) . j by EUCLID:def 4 ; :: thesis: verum

end;

len (mlt (v,z)) = n by CARD_1:def 7;
then dom (mlt (v,(0* n))) = dom (0* n) by A1, FINSEQ_3:29;
hence mlt (v,(0* n)) = 0* n by A2, FINSEQ_1:13; :: thesis: verum