set x = the Element of X;
set Y = { (n --> the Element of X) where n is Nat : verum } ;
A1: { (n --> the Element of X) where n is Nat : verum } c= X ^omega

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (n --> the Element of X) where n is Nat : verum } or a in X ^omega )
assume a in { (n --> the Element of X) where n is Nat : verum } ; :: thesis: a in X ^omega
then ex n being Nat st a = n --> the Element of X ;
hence a in X ^omega by AFINSQ_1:def 7; :: thesis: verum

end;

defpred S₁[ object , object ] means ex z being set st
( z = X & c₂ = card z );
A2: for e being object st e in { (n --> the Element of X) where n is Nat : verum } holds
ex u being object st S₁[e,u]

proof

let e be object ; :: thesis: ( e in { (n --> the Element of X) where n is Nat : verum } implies ex u being object st S₁[e,u] )
assume e in { (n --> the Element of X) where n is Nat : verum } ; :: thesis: ex u being object st S₁[e,u]
reconsider e = e as set by TARSKI:1;
take card e ; :: thesis: S₁[e, card e]
thus S₁[e, card e] ; :: thesis: verum

end;

consider f being Function such that
A3: ( dom f = { (n --> the Element of X) where n is Nat : verum } & ( for a being object st a in { (n --> the Element of X) where n is Nat : verum } holds
S₁[a,f . a] ) ) from CLASSES1:sch 1(A2);
rng f = NAT

proof

thus rng f c= NAT :: according to XBOOLE_0:def 10 :: thesis: NAT c= rng f

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng f or a in NAT )
assume a in rng f ; :: thesis: a in NAT
then consider b being object such that
A4: ( b in dom f & a = f . b ) by FUNCT_1:def 3;
consider n being Nat such that
A5: b = n --> the Element of X by A3, A4;
ex z being set st
( z = b & f . b = card z ) by A3, A4;
then a = card (dom (n --> the Element of X)) by A4, A5
.= card n
.= n ;
hence a in NAT by ORDINAL1:def 12; :: thesis: verum

end;

let n be Nat; :: according to MEMBERED:def 12 :: thesis: ( not n in NAT or n in rng f )
assume n in NAT ; :: thesis: n in rng f
A6: n --> the Element of X in { (n --> the Element of X) where n is Nat : verum } ;
then ex z being set st
( z = n --> the Element of X & f . (n --> the Element of X) = card z ) by A3;
then f . (n --> the Element of X) = card (dom (n --> the Element of X))
.= card n
.= n ;
hence n in rng f by A3, A6, FUNCT_1:def 3; :: thesis: verum

end;

hence not X ^omega is finite by A1, A3, FINSET_1:8; :: thesis: verum