let i, n 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;
A2: dom (0* n) = Seg n by FINSEQ_2:124;
( i in Seg n or not i in Seg n ) ;
then A3: (0* n) . i = 0 by A1, A2, FUNCOP_1:7, FUNCT_1:def 2;
(mlt (v,(0* n))) . i = (v . i) * ((0* n) . i) by RVSUM_1:60
.= 0 by A3 ;
hence (mlt (v,(0* n))) . i = 0 ; :: thesis: verum