let k be Element of NAT ; :: thesis: for X being non empty finite Subset of [:NAT,{k}:] ex n being non empty Element of NAT st X c= [:((Seg n) \/ {0}),{k}:]
let X be non empty finite Subset of [:NAT,{k}:]; :: thesis: ex n being non empty Element of NAT st X c= [:((Seg n) \/ {0}),{k}:]
reconsider pX = proj1 X as non empty finite Subset of NAT by FUNCT_5:11;
reconsider mpX = max pX as Element of NAT by ORDINAL1:def 12;
reconsider m = mpX + 1 as non empty Element of NAT ;
take m ; :: thesis: X c= [:((Seg m) \/ {0}),{k}:]
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in [:((Seg m) \/ {0}),{k}:] )
A1: Seg m c= (Seg m) \/ {0} by XBOOLE_1:7;
A2: {0} c= (Seg m) \/ {0} by XBOOLE_1:7;
assume A3: x in X ; :: thesis: x in [:((Seg m) \/ {0}),{k}:]
then consider x1, x2 being set such that
A4: x1 in NAT and
A5: x2 in {k} and
A6: x = [x1,x2] by ZFMISC_1:def 2;
reconsider n = x `1 as Element of NAT by A4, A6, MCART_1:7;
A7: x1 = x `1 by A6, MCART_1:7;
then n in pX by A3, A6, RELAT_1:def 4;
then ( max pX <= m & n <= max pX ) by NAT_1:11, XXREAL_2:def 8;
then A8: n <= m by XXREAL_0:2;

per cases ( 1 <= n or 0 = n ) by NAT_1:25;

suppose 1 <= n ; :: thesis: x in [:((Seg m) \/ {0}),{k}:]

then n in Seg m by A8, FINSEQ_1:1;
hence x in [:((Seg m) \/ {0}),{k}:] by A5, A6, A7, A1, ZFMISC_1:87; :: thesis: verum

end;

suppose 0 = n ; :: thesis: x in [:((Seg m) \/ {0}),{k}:]

then n in {0} by TARSKI:def 1;
hence x in [:((Seg m) \/ {0}),{k}:] by A5, A6, A7, A2, ZFMISC_1:87; :: thesis: verum

end;

end;