set seg = Seg (card D);

A1: D ** c= PFuncs ((Seg (card D)),D)

hence D ** is finite by A1; :: thesis: verum

A1: D ** c= PFuncs ((Seg (card D)),D)

proof

PFuncs ((Seg (card D)),D) is finite
by PRE_POLY:17;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in D ** or x in PFuncs ((Seg (card D)),D) )

assume x in D ** ; :: thesis: x in PFuncs ((Seg (card D)),D)

then reconsider f = x as one-to-one FinSequence of D by Def2;

A2: dom f c= Seg (card D)

hence x in PFuncs ((Seg (card D)),D) by A2, PARTFUN1:def 3; :: thesis: verum

end;assume x in D ** ; :: thesis: x in PFuncs ((Seg (card D)),D)

then reconsider f = x as one-to-one FinSequence of D by Def2;

A2: dom f c= Seg (card D)

proof

rng f c= D
;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom f or x in Seg (card D) )

assume A3: x in dom f ; :: thesis: x in Seg (card D)

then reconsider x1 = x as Nat ;

A4: x in Seg (len f) by A3, FINSEQ_1:def 3;

then A5: 1 <= x1 by FINSEQ_1:1;

x1 <= len f by A4, FINSEQ_1:1;

then A6: x1 <= card (rng f) by FINSEQ_4:62;

Segm (card (rng f)) c= Segm (card D) by CARD_1:11;

then card (rng f) <= card D by NAT_1:39;

then x1 <= card D by XXREAL_0:2, A6;

hence x in Seg (card D) by A5; :: thesis: verum

end;assume A3: x in dom f ; :: thesis: x in Seg (card D)

then reconsider x1 = x as Nat ;

A4: x in Seg (len f) by A3, FINSEQ_1:def 3;

then A5: 1 <= x1 by FINSEQ_1:1;

x1 <= len f by A4, FINSEQ_1:1;

then A6: x1 <= card (rng f) by FINSEQ_4:62;

Segm (card (rng f)) c= Segm (card D) by CARD_1:11;

then card (rng f) <= card D by NAT_1:39;

then x1 <= card D by XXREAL_0:2, A6;

hence x in Seg (card D) by A5; :: thesis: verum

hence x in PFuncs ((Seg (card D)),D) by A2, PARTFUN1:def 3; :: thesis: verum

hence D ** is finite by A1; :: thesis: verum