let D be non empty set ; :: thesis: omega c= card (D *)

defpred S_{1}[ 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_{1}[x,y]

A3: ( dom f = D * & ( for x being object st x in D * holds

S_{1}[x,f . x] ) )
from CLASSES1:sch 1(A2);

defpred S_{2}[ Nat] means $1 in f .: (D *);

A4: for n being Nat st S_{2}[n] holds

S_{2}[n + 1]

( {} = p & f . {} = len p ) by A3, FINSEQ_1:49;

then A12: S_{2}[ 0 ]
by A3, A1, FUNCT_1:def 6;

A13: for n being Nat holds S_{2}[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

defpred S

( $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

proof

consider f being Function such that
let x be object ; :: thesis: ( x in D * implies ex y being object st S_{1}[x,y] )

assume x in D * ; :: thesis: ex y being object st S_{1}[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_{1}[x,y]

take p ; :: thesis: ( x = p & y = len p )

thus ( x = p & y = len p ) ; :: thesis: verum

end;assume x in D * ; :: thesis: ex y being object st S

then reconsider p = x as Element of D * ;

reconsider p = p as FinSequence ;

reconsider y = len p as set ;

take y ; :: thesis: S

take p ; :: thesis: ( x = p & y = len p )

thus ( x = p & y = len p ) ; :: thesis: verum

A3: ( dom f = D * & ( for x being object st x in D * holds

S

defpred S

A4: for n being Nat st S

S

proof

ex p being FinSequence st
set y = the Element of D;

let n be Nat; :: thesis: ( S_{2}[n] implies S_{2}[n + 1] )

assume n in f .: (D *) ; :: thesis: S_{2}[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_{2}[n + 1]
by A3, A11, A10, FUNCT_1:def 6; :: thesis: verum

end;let n be Nat; :: thesis: ( S

assume n in f .: (D *) ; :: thesis: S

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

( {} = p & f . {} = len p ) by A3, FINSEQ_1:49;

then A12: S

A13: for n being Nat holds S

NAT c= f .: (D *) by A13;

hence omega c= card (D *) by CARD_1:47, CARD_1:66; :: thesis: verum