reconsider z = 0 , o = 1 as Element of NAT ;
set D = NAT \ {o};
( z in NAT & not z in {o} ) ;
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;
A1: ( zz in {zz} & dom g = {zz} & dom f = NAT \ {o} ) by TARSKI:def 1;
dom (f +* g) = (NAT \ {o}) null {zz} by FUNCT_4:def 1;
then ( rng (f +* g) c= INT & dom (f +* g) = NAT \ {o} ) ;
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 #);
A2: 0. Language-like(# NAT,z,o,aa #) <> 1. Language-like(# NAT,z,o,aa #) ;
aa . z = g . zz by A1, FUNCT_4:13
.= - 2 by A1, FUNCOP_1:7 ;
then A3: aa . (TheEqSymbOf Language-like(# NAT,z,o,aa #)) = - 2 ;

now :: thesis: for x being object st x in (NAT \ {o}) \ {z} holds
x in aa " {0}

let x be object ; :: thesis: ( x in (NAT \ {o}) \ {z} implies x in aa " {0} )
assume x in (NAT \ {o}) \ {z} ; :: thesis: x in aa " {0}
then A4: ( x in NAT \ {o} & not x in {zz} ) ;
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 ;
then ( x in dom aa & aa . x in {0} ) by TARSKI:def 1, A4, FUNCT_2: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;
( E is infinite & (aa " {0}) \/ E = (aa " {0}) null E ) ;
then LettersOf Language-like(# NAT,z,o,aa #) is infinite ;
then reconsider IT = Language-like(# NAT,z,o,aa #) as Language by A2, STRUCT_0:def 8, A3, Def23;
take IT ; :: thesis: IT is countable
thus IT is countable by ORDERS_4:def 2; :: thesis: verum