len x >= 0 + 1 by A1, NAT_1:13;
then 1 in dom x by FINSEQ_3:27;
then A2: x . 1 in rng x by FUNCT_1:def 5;
rng x c= NAT by FINSEQ_1:def 4;
then reconsider n = x . 1 as Element of NAT by A2;
take n + 1 ; :: thesis: ex n being Element of NAT st
( n + 1 = n + 1 & x . 1 = n )
take n ; :: thesis: ( n + 1 = n + 1 & x . 1 = n )
thus ( n + 1 = n + 1 & x . 1 = n ) ; :: thesis: verum