defpred S₁[ set ] means ( ex m being non empty Element of NAT st
( m <= n & $1 = PFArt m,k ) or $1 = PFCrt n,k );
consider X being set such that
A1: for x being set holds
( x in X iff ( x in PFuncs NAT ,{k} & S₁[x] ) ) from XBOOLE_0:sch 1();
A2: X c= bool [:(Seg ((2 * n) + 1)),{k}:]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in bool [:(Seg ((2 * n) + 1)),{k}:] )
assume A3: x in X ; :: thesis: x in bool [:(Seg ((2 * n) + 1)),{k}:]

per cases ( ex m being non empty Element of NAT st
( m <= n & x = PFArt m,k ) or x = PFCrt n,k ) by A1, A3;

suppose A4: ex m being non empty Element of NAT st
( m <= n & x = PFArt m,k ) ; :: thesis: x in bool [:(Seg ((2 * n) + 1)),{k}:]

A5: 2 * n <= (2 * n) + 1 by NAT_1:11;
consider m being non empty Element of NAT such that
A6: m <= n and
A7: x = PFArt m,k by A4;
2 * m <= 2 * n by A6, NAT_1:4;
then A8: 2 * m <= (2 * n) + 1 by A5, XXREAL_0:2;
x c= [:(Seg ((2 * n) + 1)),{k}:]

proof

let t be set ; :: according to TARSKI:def 3 :: thesis: ( not t in x or t in [:(Seg ((2 * n) + 1)),{k}:] )
assume A9: t in x ; :: thesis: t in [:(Seg ((2 * n) + 1)),{k}:]

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

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

then consider m1 being odd Element of NAT such that
A10: m1 <= 2 * m and
A11: [m1,k] = t ;
A12: 1 <= m1 by ABIAN:12;
m1 <= (2 * n) + 1 by A8, A10, XXREAL_0:2;
then m1 in Seg ((2 * n) + 1) by A12, FINSEQ_1:3;
hence t in [:(Seg ((2 * n) + 1)),{k}:] by A11, ZFMISC_1:129; :: thesis: verum

end;

suppose A13: [(2 * m),k] = t ; :: thesis: t in [:(Seg ((2 * n) + 1)),{k}:]

m <= 2 * m by XREAL_1:153;
then 1 <= 2 * m by NAT_1:14;
then 2 * m in Seg ((2 * n) + 1) by A8, FINSEQ_1:3;
hence t in [:(Seg ((2 * n) + 1)),{k}:] by A13, ZFMISC_1:129; :: thesis: verum

end;

end;

end;

hence x in bool [:(Seg ((2 * n) + 1)),{k}:] ; :: thesis: verum

end;

suppose A14: x = PFCrt n,k ; :: thesis: x in bool [:(Seg ((2 * n) + 1)),{k}:]

x c= [:(Seg ((2 * n) + 1)),{k}:]

proof

let t be set ; :: according to TARSKI:def 3 :: thesis: ( not t in x or t in [:(Seg ((2 * n) + 1)),{k}:] )
assume t in x ; :: thesis: t in [:(Seg ((2 * n) + 1)),{k}:]
then consider m being odd Element of NAT such that
A15: m <= (2 * n) + 1 and
A16: [m,k] = t by A14, Def3;
1 <= m by ABIAN:12;
then m in Seg ((2 * n) + 1) by A15, FINSEQ_1:3;
hence t in [:(Seg ((2 * n) + 1)),{k}:] by A16, ZFMISC_1:129; :: thesis: verum

end;

hence x in bool [:(Seg ((2 * n) + 1)),{k}:] ; :: thesis: verum

end;

end;

end;

X c= PFuncs NAT ,{k}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in PFuncs NAT ,{k} )
assume x in X ; :: thesis: x in PFuncs NAT ,{k}
hence x in PFuncs NAT ,{k} by A1; :: thesis: verum

end;

then reconsider X = X as Element of Fin (PFuncs NAT ,{k}) by A2, FINSUB_1:def 5;
take X ; :: thesis: for x being set holds
( x in X iff ( ex m being non empty Element of NAT st
( m <= n & x = PFArt m,k ) or x = PFCrt n,k ) )
let x be set ; :: thesis: ( x in X iff ( ex m being non empty Element of NAT st
( m <= n & x = PFArt m,k ) or x = PFCrt n,k ) )
thus ( not x in X or ex m being non empty Element of NAT st
( m <= n & x = PFArt m,k ) or x = PFCrt n,k ) by A1; :: thesis: ( ( ex m being non empty Element of NAT st
( m <= n & x = PFArt m,k ) or x = PFCrt n,k ) implies x in X )
assume ( ex m being non empty Element of NAT st
( m <= n & x = PFArt m,k ) or x = PFCrt n,k ) ; :: thesis: x in X
hence x in X by A1; :: thesis: verum