let X be set ; :: thesis: for P being finite without_zero Subset of NAT st X c= P holds
card X = card ((Sgm P) " X)
let P be finite without_zero Subset of NAT; :: thesis: ( X c= P implies card X = card ((Sgm P) " X) )
assume A1: X c= P ; :: thesis: card X = card ((Sgm P) " X)
A2: ex n being Nat st P c= Seg n by Th43;
then rng (Sgm P) = P by FINSEQ_1:def 13;
then A3: (Sgm P) .: ((Sgm P) " X) = X by A1, FUNCT_1:77;
A4: (Sgm P) " X c= dom (Sgm P) by RELAT_1:132;
Sgm P is one-to-one by A2, FINSEQ_3:92;
then X,(Sgm P) " X are_equipotent by A3, A4, CARD_1:33;
hence card X = card ((Sgm P) " X) by CARD_1:5; :: thesis: verum