defpred S₁[ set ] means ( ex m being odd Element of NAT st
( m <= 2 * n & [m,k] = $1 ) or [(2 * n),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 X9 = X as Function by GRFUNC_1:6;
( dom X9 c= NAT & rng X9 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 & [m,k] = x ) or [(2 * n),k] = x ) )
let x be set ; :: thesis: ( x in X iff ( ex m being odd Element of NAT st
( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) )
thus ( not x in X or ex m being odd Element of NAT st
( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) by A1; :: thesis: ( ( ex m being odd Element of NAT st
( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) implies x in X )
assume A3: ( ex m being odd Element of NAT st
( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) ; :: thesis: x in X

per cases ( ex m being odd Element of NAT st
( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) by A3;

suppose ex m being odd Element of NAT st
( m <= 2 * n & [m,k] = x ) ; :: thesis: x in X

then x in [:NAT ,{k}:] by ZFMISC_1:129;
hence x in X by A1, A3; :: thesis: verum

end;

suppose A4: [(2 * n),k] = x ; :: thesis: x in X

then x in [:NAT ,{k}:] by ZFMISC_1:129;
hence x in X by A1, A4; :: thesis: verum

end;

end;