reconsider z = 0 , o = 1 as Element of NAT ;
set D = NAT \ {o};
( z in NAT & not z in {o} ) by TARSKI:def 1;
then reconsider zz = z as Element of NAT \ {o} by XBOOLE_0:def 5;
reconsider f = (NAT \ {o}) --> 0, g = zz .--> (- 2) as INT -valued Function ;
set a = f +* g;
B0: ( zz in {zz} & dom g = {zz} & dom f = NAT \ {o} ) by FUNCOP_1:13, TARSKI:def 1;
then dom (f +* g) = (NAT \ {o}) null {zz} by FUNCT_4:def 1;
then ( rng (f +* g) c= INT & dom (f +* g) = NAT \ {o} ) by RELAT_1:def 19;
then f +* g is Element of Funcs ((NAT \ {o}),INT) by FUNCT_2:def 2;
then reconsider aa = f +* g as Function of (NAT \ {o}),INT ;
set IT = Language-like(# NAT,z,o,aa #);
Z2: 0. Language-like(# NAT,z,o,aa #) <> 1. Language-like(# NAT,z,o,aa #) ;
aa . z = g . zz by B0, FUNCT_4:13
.= - 2 by B0, FUNCOP_1:7 ;
then B1: aa . (TheEqSymbOf Language-like(# NAT,z,o,aa #)) = - 2 ;

now

let x be set ; :: thesis: ( x in (NAT \ {o}) \ {z} implies x in aa " {0} )
assume Z1: x in (NAT \ {o}) \ {z} ; :: thesis: x in aa " {0}
then C0: ( x in NAT \ {o} & not x in {zz} ) by XBOOLE_0:def 5;
then ( x in dom aa & not x in dom g ) by FUNCT_2:def 1;
then aa . x = f . x by FUNCT_4:11
.= 0 by Z1, FUNCOP_1:7 ;
then ( x in dom aa & aa . x in {0} ) by C0, FUNCT_2:def 1, TARSKI:def 1;
hence x in aa " {0} by FUNCT_1:def 7; :: thesis: verum

end;

then reconsider E = (NAT \ {o}) \ {z} as Subset of (aa " {0}) by TARSKI:def 3;
( not E is finite & (aa " {0}) \/ E = (aa " {0}) null E ) ;
then not LettersOf Language-like(# NAT,z,o,aa #) is finite ;
then reconsider IT = Language-like(# NAT,z,o,aa #) as Language by Z2, B1, DefEligible, STRUCT_0:def 8;
take IT ; :: thesis: IT is countable
thus IT is countable by ORDERS_4:def 2; :: thesis: verum