PFArt (n,k) c= [:((Seg (2 * n)) \/ {0}),{k}:]

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in PFArt (n,k) or t in [:((Seg (2 * n)) \/ {0}),{k}:] )
assume A1: t in PFArt (n,k) ; :: thesis: t in [:((Seg (2 * n)) \/ {0}),{k}:]

per cases ( ex m1 being odd Element of NAT st
( m1 <= 2 * n & [m1,k] = t ) or [(2 * n),k] = t ) by A1, Def2;

suppose ex m1 being odd Element of NAT st
( m1 <= 2 * n & [m1,k] = t ) ; :: thesis: t in [:((Seg (2 * n)) \/ {0}),{k}:]

then consider m1 being odd Element of NAT such that
A2: m1 <= 2 * n and
A3: [m1,k] = t ;
1 <= m1 by ABIAN:12;
then m1 in Seg (2 * n) by A2, FINSEQ_1:1;
then m1 in (Seg (2 * n)) \/ {0} by XBOOLE_0:def 3;
hence t in [:((Seg (2 * n)) \/ {0}),{k}:] by A3, ZFMISC_1:106; :: thesis: verum

end;

suppose A4: [(2 * n),k] = t ; :: thesis: t in [:((Seg (2 * n)) \/ {0}),{k}:]

now :: thesis: t in [:((Seg (2 * n)) \/ {0}),{k}:]

per cases ( not n is zero or n is zero ) ;

suppose A5: not n is zero ; :: thesis: t in [:((Seg (2 * n)) \/ {0}),{k}:]

A6: n <= 2 * n by XREAL_1:151;
1 <= n by A5, NAT_1:14;
then 1 <= 2 * n by A6, XXREAL_0:2;
then 2 * n in Seg (2 * n) by FINSEQ_1:1;
then 2 * n in (Seg (2 * n)) \/ {0} by XBOOLE_0:def 3;
hence t in [:((Seg (2 * n)) \/ {0}),{k}:] by A4, ZFMISC_1:106; :: thesis: verum

end;

suppose n is zero ; :: thesis: t in [:((Seg (2 * n)) \/ {0}),{k}:]

then 2 * n in {0} by TARSKI:def 1;
then 2 * n in (Seg (2 * n)) \/ {0} by XBOOLE_0:def 3;
hence t in [:((Seg (2 * n)) \/ {0}),{k}:] by A4, ZFMISC_1:106; :: thesis: verum

end;

end;

end;

hence t in [:((Seg (2 * n)) \/ {0}),{k}:] ; :: thesis: verum

end;

end;

end;

hence PFArt (n,k) is finite ; :: thesis: verum