defpred S₁[ set ] means ex m being odd Element of NAT st
( m <= (2 * n) + 1 & [m,k] = $1 );
A5: for X1, X2 being Element of PFuncs (NAT,{k}) st ( for x being set holds
( x in X1 iff S₁[x] ) ) & ( for x being set holds
( x in X2 iff S₁[x] ) ) holds
X1 = X2 from LMOD_7:sch 1();
let X1, X2 be Element of PFuncs (NAT,{k}); :: thesis: ( ( for x being set holds
( x in X1 iff ex m being odd Element of NAT st
( m <= (2 * n) + 1 & [m,k] = x ) ) ) & ( for x being set holds
( x in X2 iff ex m being odd Element of NAT st
( m <= (2 * n) + 1 & [m,k] = x ) ) ) implies X1 = X2 )
assume ( ( for x being set holds
( x in X1 iff S₁[x] ) ) & ( for x being set holds
( x in X2 iff S₁[x] ) ) ) ; :: thesis: X1 = X2
hence X1 = X2 by A5; :: thesis: verum