let n, k be Element of NAT ; :: thesis: for f being Function of (n + 1),k st k <> 0 & f " {(f . n)} <> {n} holds
ex m being Element of NAT st
( m in f " {(f . n)} & m <> n )
let f be Function of (n + 1),k; :: thesis: ( k <> 0 & f " {(f . n)} <> {n} implies ex m being Element of NAT st
( m in f " {(f . n)} & m <> n ) )
assume that
A1: k <> 0 and
A2: f " {(f . n)} <> {n} ; :: thesis: ex m being Element of NAT st
( m in f " {(f . n)} & m <> n )
( n < n + 1 & dom f = n + 1 ) by A1, FUNCT_2:def 1, NAT_1:13;
then ( n in dom f & f . n in {(f . n)} ) by NAT_1:45, TARSKI:def 1;
then n in f " {(f . n)} by FUNCT_1:def 13;
then ex m being set st
( m in f " {(f . n)} & m <> n ) by A2, ZFMISC_1:41;
hence ex m being Element of NAT st
( m in f " {(f . n)} & m <> n ) ; :: thesis: verum