let D be non empty set ; :: thesis: omega c= card (D *)
defpred S1[ 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 S1[x,y]
proof
let x be object ; :: thesis: ( x in D * implies ex y being object st S1[x,y] )
assume x in D * ; :: thesis: ex y being object st S1[x,y]
then reconsider p = x as Element of D * ;
reconsider p = p as FinSequence ;
reconsider y = len p as set ;
take y ; :: thesis: S1[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
S1[x,f . x] ) ) from defpred S2[ Nat] means \$1 in f .: (D *);
A4: for n being Nat st S2[n] holds
S2[n + 1]
proof
set y = the Element of D;
let n be Nat; :: thesis: ( S2[n] implies S2[n + 1] )
assume n in f .: (D *) ; :: thesis: S2[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 ;
A10: len (p ^ <* the Element of D*>) = n + (len <* the Element of D*>) by
.= 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 S2[n + 1] by ; :: thesis: verum
end;
ex p being FinSequence st
( {} = p & f . {} = len p ) by ;
then A12: S2[ 0 ] by ;
A13: for n being Nat holds S2[n] from NAT_1:sch 2(A12, A4);
NAT c= f .: (D *) by A13;
hence omega c= card (D *) by ; :: thesis: verum