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

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