let k, n be Nat; :: thesis: for f being Function of (Segm (n + 1)),(Segm k) st k <> 0 & f " {(f . n)} <> {n} holds
ex m being Nat st
( m in f " {(f . n)} & m <> n )
let f be Function of (Segm (n + 1)),(Segm k); :: thesis: ( k <> 0 & f " {(f . n)} <> {n} implies ex m being Nat st
( m in f " {(f . n)} & m <> n ) )
assume that
A1: k <> 0 and
A2: f " {(f . n)} <> {n} ; :: thesis: ex m being Nat st
( m in f " {(f . n)} & m <> n )
A3: n < n + 1 by NAT_1:13;
A4: f . n in {(f . n)} by TARSKI:def 1;
dom f = n + 1 by A1, FUNCT_2:def 1;
then n in dom f by A3, NAT_1:44;
then n in f " {(f . n)} by A4, FUNCT_1:def 7;
then ex m being object st
( m in f " {(f . n)} & m <> n ) by A2, ZFMISC_1:35;
hence ex m being Nat st
( m in f " {(f . n)} & m <> n ) ; :: thesis: verum