let K be non zero Nat; :: thesis: for y being Tuple of K, BOOLEAN st y = 0* K holds
for n being non zero Nat st n <= K holds
y /. n = 0
let y be Tuple of K, BOOLEAN ; :: thesis: ( y = 0* K implies for n being non zero Nat st n <= K holds
y /. n = 0 )
assume AS1: y = 0* K ; :: thesis: for n being non zero Nat st n <= K holds
y /. n = 0
let n be non zero Nat; :: thesis: ( n <= K implies y /. n = 0 )
assume AS2: n <= K ; :: thesis: y /. n = 0
A1: len y = K by CARD_1:def 7;
0 < n ;
then 1 + 0 <= n by NAT_1:13;
then n in Seg K by FINSEQ_1:1, AS2;
then n in dom y by A1, FINSEQ_1:def 3;
hence y /. n = y . n by PARTFUN1:def 6
.= 0 by AS1 ;
:: thesis: verum