let n, i be Element of NAT ; :: thesis: ( i in Seg n implies Proj (0.REAL n),i = 0 )
assume A1: i in Seg n ; :: thesis: Proj (0.REAL n),i = 0
len (0* n) = n by FINSEQ_2:109;
then A2: i in dom (0* n) by A1, FINSEQ_1:def 3;
Proj (0.REAL n),i = (0* n) /. i by Def1
.= (0* n) . i by A2, PARTFUN1:def 8
.= 0 by A1, FUNCOP_1:13 ;
hence Proj (0.REAL n),i = 0 ; :: thesis: verum