let n, i be Nat; :: thesis: for k being Complex st n <> i holds
((n --> 0) ^ <%k%>) . i = 0
let k be Complex; :: thesis: ( n <> i implies ((n --> 0) ^ <%k%>) . i = 0 )
assume A1: n <> i ; :: thesis: ((n --> 0) ^ <%k%>) . i = 0

per cases ( n > i or n < i ) by A1, XXREAL_0:1;

suppose n > i ; :: thesis: ((n --> 0) ^ <%k%>) . i = 0

then len (n --> 0) > i ;
then ((n --> 0) ^ <%k%>) . i = (n --> 0) . i by AFINSQ_1:51
.= 0 ;
hence ((n --> 0) ^ <%k%>) . i = 0 ; :: thesis: verum

end;

suppose n < i ; :: thesis: ((n --> 0) ^ <%k%>) . i = 0

then i >= n + 1 by INT_1:7;
then i >= len ((n --> 0) ^ <%k%>) by CARD_1:def 7;
then not i in dom ((n --> 0) ^ <%k%>) by AFINSQ_1:86;
hence ((n --> 0) ^ <%k%>) . i = 0 by FUNCT_1:def 2; :: thesis: verum

end;

end;