let k, n be Nat; for f being Function of (Segm n),(Segm k)
for g being Function of (Segm (n + 1)),(Segm k) st f is onto & f is "increasing & f = g | (Segm n) & g . n < k holds
( g is onto & g is "increasing & g " {(g . n)} <> {n} )
let f be Function of (Segm n),(Segm k); for g being Function of (Segm (n + 1)),(Segm k) st f is onto & f is "increasing & f = g | (Segm n) & g . n < k holds
( g is onto & g is "increasing & g " {(g . n)} <> {n} )
let g be Function of (Segm (n + 1)),(Segm k); ( f is onto & f is "increasing & f = g | (Segm n) & g . n < k implies ( g is onto & g is "increasing & g " {(g . n)} <> {n} ) )
assume that
A1:
( f is onto & f is "increasing )
and
A2:
f = g | (Segm n)
and
A3:
g . n < k
; ( g is onto & g is "increasing & g " {(g . n)} <> {n} )
k = rng f
by A1, FUNCT_2:def 3;
then consider x being object such that
A4:
x in dom f
and
A5:
f . x = g . n
by A3, FUNCT_1:def 3;
g . n = g . x
by A2, A4, A5, FUNCT_1:47;
then A6:
g . x in {(g . n)}
by TARSKI:def 1;
k c= rng g
proof
n <= n + 1
by NAT_1:13;
then A7:
Segm n c= Segm (n + 1)
by NAT_1:39;
(
n = 0 iff
k = 0 )
by A1;
then A8:
dom f = n
by FUNCT_2:def 1;
let x9 be
object ;
TARSKI:def 3 ( not x9 in k or x9 in rng g )
assume A9:
x9 in k
;
x9 in rng g
k is
Subset of
NAT
by Th8;
then reconsider x =
x9 as
Element of
NAT by A9;
rng f = k
by A1, FUNCT_2:def 3;
then consider y being
object such that A10:
y in dom f
and A11:
f . y = x
by A9, FUNCT_1:def 3;
A12:
dom g = n + 1
by A3, FUNCT_2:def 1;
f . y = g . y
by A2, A10, FUNCT_1:47;
hence
x9 in rng g
by A10, A11, A8, A7, A12, FUNCT_1:def 3;
verum
end;
then
k = rng g
;
hence
g is onto
by FUNCT_2:def 3; ( g is "increasing & g " {(g . n)} <> {n} )
k = k + 0
;
then
for i, j being Nat st i in rng g & j in rng g & i < j holds
min* (g " {i}) < min* (g " {j})
by A1, A2, Th39;
hence
g is "increasing
by A3; g " {(g . n)} <> {n}
n <= n + 1
by NAT_1:11;
then A13:
Segm n c= Segm (n + 1)
by NAT_1:39;
reconsider nn = n as set ;
A:
not nn in nn
;
A14:
x in n
by A4;
then A15:
x <> n
by A;
dom g = n + 1
by A3, FUNCT_2:def 1;
then
x in g " {(g . n)}
by A14, A13, A6, FUNCT_1:def 7;
hence
g " {(g . n)} <> {n}
by A15, TARSKI:def 1; verum