let n, i be Element of NAT ; :: thesis: ( i in Seg n implies Proj (0. (TOP-REAL n)),i = 0 )
assume A1: i in Seg n ; :: thesis: Proj (0. (TOP-REAL n)),i = 0
len (0* n) = n by FINSEQ_1:def 18;
then A2: i in dom (0* n) by A1, FINSEQ_1:def 3;
0. (TOP-REAL n) = 0* n by EUCLID:74;
then Proj (0. (TOP-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. (TOP-REAL n)),i = 0 ; :: thesis: verum