let X be set ; :: thesis: for P being finite without_zero Subset of NAT holds (Sgm P) " X is finite without_zero Subset of NAT
let P be finite without_zero Subset of NAT; :: thesis: (Sgm P) " X is finite without_zero Subset of NAT
A1: (Sgm P) " X c= dom (Sgm P) by RELAT_1:132;
ex k being Nat st P c= Seg k by Th43;
then dom (Sgm P) = Seg (card P) by FINSEQ_3:40;
then not 0 in (Sgm P) " X by A1;
hence (Sgm P) " X is finite without_zero Subset of NAT by A1, MEASURE6:def 2, XBOOLE_1:1; :: thesis: verum