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