defpred S₁[ object ] 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 object holds
( x in X iff ( x in [:NAT,{k}:] & S₁[x] ) ) from XBOOLE_0:sch 1();
A2: X c= [:NAT,{k}:] by A1;
then reconsider X9 = X as Function by GRFUNC_1:1;
( dom X9 c= NAT & rng X9 c= {k} ) by A2, SYSREL:3;
then reconsider X = X as Element of PFuncs (NAT,{k}) by PARTFUN1:def 3;
take X ; :: thesis: for x being object 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 object ; :: 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
A4: 2 * n in NAT by ORDINAL1:def 12;

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:106;
hence x in X by A1, A3; :: thesis: verum

end;

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

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

end;

end;