let k, n be Nat; :: thesis: for f being Function of (Segm (n + 1)),(Segm k)

for g being Function of (Segm n),(Segm k) st f is onto & f is "increasing & f " {(f . n)} <> {n} & f | n = g holds

( g is onto & g is "increasing )

let f be Function of (Segm (n + 1)),(Segm k); :: thesis: for g being Function of (Segm n),(Segm k) st f is onto & f is "increasing & f " {(f . n)} <> {n} & f | n = g holds

( g is onto & g is "increasing )

let g be Function of (Segm n),(Segm k); :: thesis: ( f is onto & f is "increasing & f " {(f . n)} <> {n} & f | n = g implies ( g is onto & g is "increasing ) )

assume that

A1: ( f is onto & f is "increasing ) and

A2: f " {(f . n)} <> {n} and

A3: f | n = g ; :: thesis: ( g is onto & g is "increasing )

for g being Function of (Segm n),(Segm k) st f is onto & f is "increasing & f " {(f . n)} <> {n} & f | n = g holds

( g is onto & g is "increasing )

let f be Function of (Segm (n + 1)),(Segm k); :: thesis: for g being Function of (Segm n),(Segm k) st f is onto & f is "increasing & f " {(f . n)} <> {n} & f | n = g holds

( g is onto & g is "increasing )

let g be Function of (Segm n),(Segm k); :: thesis: ( f is onto & f is "increasing & f " {(f . n)} <> {n} & f | n = g implies ( g is onto & g is "increasing ) )

assume that

A1: ( f is onto & f is "increasing ) and

A2: f " {(f . n)} <> {n} and

A3: f | n = g ; :: thesis: ( g is onto & g is "increasing )

now :: thesis: ( g is onto & g is "increasing )end;

hence
( g is onto & g is "increasing )
; :: thesis: verumper cases
( k = 0 or k > 0 )
;

end;

suppose A4:
k > 0
; :: thesis: ( g is onto & g is "increasing )

A5:
rng f = k
by A1, FUNCT_2:def 3;

end;now :: thesis: ( g is onto & g is "increasing )

hence
( g is onto & g is "increasing )
; :: thesis: verum
k = k + 0
;

then A6: 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, A3, Th36;

A7: k c= rng g

( n = 0 iff k = 0 ) by A4, A7;

hence ( g is onto & g is "increasing ) by A20, A6, FUNCT_2:def 3; :: thesis: verum

end;then A6: 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, A3, Th36;

A7: k c= rng g

proof

then A20:
rng g = k
;
let k1 be object ; :: according to TARSKI:def 3 :: thesis: ( not k1 in k or k1 in rng g )

assume A8: k1 in k ; :: thesis: k1 in rng g

consider x being object such that

A9: x in dom f and

A10: f . x = k1 by A5, A8, FUNCT_1:def 3;

dom f = n + 1 by A8, FUNCT_2:def 1;

then reconsider x = x as Element of NAT by A9;

x < n + 1 by A9, NAT_1:44;

then A11: x <= n by NAT_1:13;

end;assume A8: k1 in k ; :: thesis: k1 in rng g

consider x being object such that

A9: x in dom f and

A10: f . x = k1 by A5, A8, FUNCT_1:def 3;

dom f = n + 1 by A8, FUNCT_2:def 1;

then reconsider x = x as Element of NAT by A9;

x < n + 1 by A9, NAT_1:44;

then A11: x <= n by NAT_1:13;

now :: thesis: k1 in rng gend;

hence
k1 in rng g
; :: thesis: verumper cases
( x < n or x = n )
by A11, XXREAL_0:1;

end;

suppose A12:
x < n
; :: thesis: k1 in rng g

A13:
dom g = n
by A4, FUNCT_2:def 1;

A14: x in Segm n by A12, NAT_1:44;

then g . x = f . x by A3, A13, FUNCT_1:47;

hence k1 in rng g by A10, A14, A13, FUNCT_1:def 3; :: thesis: verum

end;A14: x in Segm n by A12, NAT_1:44;

then g . x = f . x by A3, A13, FUNCT_1:47;

hence k1 in rng g by A10, A14, A13, FUNCT_1:def 3; :: thesis: verum

suppose
x = n
; :: thesis: k1 in rng g

then consider m being Nat such that

A15: m in f " {k1} and

A16: m <> n by A2, A4, A10, Th35;

f . m in {k1} by A15, FUNCT_1:def 7;

then A17: f . m = k1 by TARSKI:def 1;

m in dom f by A15, FUNCT_1:def 7;

then m < n + 1 by NAT_1:44;

then m <= n by NAT_1:13;

then m < n by A16, XXREAL_0:1;

then A18: m in Segm n by NAT_1:44;

A19: n = dom g by A4, FUNCT_2:def 1;

then g . m = f . m by A3, A18, FUNCT_1:47;

hence k1 in rng g by A18, A19, A17, FUNCT_1:def 3; :: thesis: verum

end;A15: m in f " {k1} and

A16: m <> n by A2, A4, A10, Th35;

f . m in {k1} by A15, FUNCT_1:def 7;

then A17: f . m = k1 by TARSKI:def 1;

m in dom f by A15, FUNCT_1:def 7;

then m < n + 1 by NAT_1:44;

then m <= n by NAT_1:13;

then m < n by A16, XXREAL_0:1;

then A18: m in Segm n by NAT_1:44;

A19: n = dom g by A4, FUNCT_2:def 1;

then g . m = f . m by A3, A18, FUNCT_1:47;

hence k1 in rng g by A18, A19, A17, FUNCT_1:def 3; :: thesis: verum

( n = 0 iff k = 0 ) by A4, A7;

hence ( g is onto & g is "increasing ) by A20, A6, FUNCT_2:def 3; :: thesis: verum