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

proof

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

end;

then reconsider X' = X as Function by GRFUNC_1:6;
( dom X' c= NAT & rng X' c= {k} ) by A2, SYSREL:15;
then reconsider X = X as Element of PFuncs NAT ,{k} by PARTFUN1:def 5;
take X ; :: thesis: for x being set holds
( x in X iff ex m being odd Element of NAT st
( m <= (2 * n) + 1 & [m,k] = x ) )
let x be set ; :: thesis: ( x in X iff ex m being odd Element of NAT st
( m <= (2 * n) + 1 & [m,k] = x ) )
thus ( x in X implies ex m being odd Element of NAT st
( m <= (2 * n) + 1 & [m,k] = x ) ) by A1; :: thesis: ( ex m being odd Element of NAT st
( m <= (2 * n) + 1 & [m,k] = x ) implies x in X )
given m being odd Element of NAT such that A3: ( m <= (2 * n) + 1 & [m,k] = x ) ; :: thesis: x in X
x in [:NAT ,{k}:] by A3, ZFMISC_1:129;
hence x in X by A1, A3; :: thesis: verum