let n, i be Element of NAT ; :: thesis: ( i in Seg n implies (0. (TOP-REAL n)) /. i = 0 )
assume A1: i in Seg n ; :: thesis: (0. (TOP-REAL n)) /. i = 0
len (0* n) = n by CARD_1:def 7;
then A2: i in dom (0* n) by A1, FINSEQ_1:def 3;
(0. (TOP-REAL n)) /. i = (0* n) /. i by EUCLID:70
.= (0* n) . i by A2, PARTFUN1:def 6
.= 0 by A1, FUNCOP_1:7 ;
hence (0. (TOP-REAL n)) /. i = 0 ; :: thesis: verum