let n, i be Nat; :: thesis: for v being Element of n -tuples_on REAL holds (mlt v,(0* n)) . i = 0
let v be Element of n -tuples_on REAL ; :: thesis: (mlt v,(0* n)) . i = 0
A1: 0* n = n |-> 0 by EUCLID:def 4;
set v0 = (0* n) . i;
A3: dom (0* n) = Seg n by FINSEQ_2:144;
( i in Seg n or not i in Seg n ) ;
then A2: (0* n) . i = 0 by A1, A3, FUNCOP_1:13, FUNCT_1:def 4;
(mlt v,(0* n)) . i = (v . i) * ((0* n) . i) by RVSUM_1:87
.= 0 by A2 ;
hence (mlt v,(0* n)) . i = 0 ; :: thesis: verum