let D be non empty set ; :: thesis: omega c= card (D *)
defpred S₁[ object , object ] means ex p being FinSequence st
( $1 = p & $2 = len p );
A1: ( {} in D * & len {} = 0 ) by FINSEQ_1:49;
A2: for x being object st x in D * holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis: ( x in D * implies ex y being object st S₁[x,y] )
assume x in D * ; :: thesis: ex y being object st S₁[x,y]
then reconsider p = x as Element of D * ;
reconsider p = p as FinSequence ;
reconsider y = len p as set ;
take y ; :: thesis: S₁[x,y]
take p ; :: thesis: ( x = p & y = len p )
thus ( x = p & y = len p ) ; :: thesis: verum

end;

consider f being Function such that
A3: ( dom f = D * & ( for x being object st x in D * holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(A2);
defpred S₂[ Nat] means $1 in f .: (D *);
A4: for n being Nat st S₂[n] holds
S₂[n + 1]

proof

set y = the Element of D;
let n be Nat; :: thesis: ( S₂[n] implies S₂[n + 1] )
assume n in f .: (D *) ; :: thesis: S₂[n + 1]
then consider x being object such that
A5: x in dom f and
A6: x in D * and
A7: n = f . x by FUNCT_1:def 6;
consider p being FinSequence such that
A8: x = p and
A9: n = len p by A3, A5, A7;
reconsider p = p as FinSequence of D by A6, A8, FINSEQ_1:def 11;
A10: len (p ^ <* the Element of D*>) = n + (len <* the Element of D*>) by A9, FINSEQ_1:22
.= n + 1 by FINSEQ_1:40 ;
A11: p ^ <* the Element of D*> in D * by FINSEQ_1:def 11;
then ex q being FinSequence st
( p ^ <* the Element of D*> = q & f . (p ^ <* the Element of D*>) = len q ) by A3;
hence S₂[n + 1] by A3, A11, A10, FUNCT_1:def 6; :: thesis: verum

end;

ex p being FinSequence st
( {} = p & f . {} = len p ) by A3, FINSEQ_1:49;
then A12: S₂[ 0 ] by A3, A1, FUNCT_1:def 6;
A13: for n being Nat holds S₂[n] from NAT_1:sch 2(A12, A4);
NAT c= f .: (D *) by A13;
hence omega c= card (D *) by CARD_1:47, CARD_1:66; :: thesis: verum