defpred S₁[ object ] 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 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) + 1 & [m,k] = x ) )
let x be object ; :: 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 and
A4: [m,k] = x ; :: thesis: x in X
x in [:NAT,{k}:] by A4, ZFMISC_1:106;
hence x in X by A1, A3, A4; :: thesis: verum