set seg = Seg (card D);
A1: D ** c= PFuncs ((Seg (card D)),D)
proof
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)
proof
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;
rng f c= D ;
hence x in PFuncs ((Seg (card D)),D) by A2, PARTFUN1:def 3; :: thesis: verum
end;
PFuncs ((Seg (card D)),D) is finite by PRE_POLY:17;
hence D ** is finite by A1; :: thesis: verum