theorem Th35: :: STIRL2_1:35

for k, n being Nat
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 )