let k, n be Nat; :: thesis: for f being Function of (Segm n),(Segm k) st f is onto & f is "increasing & n = k holds

f = id n

let f be Function of (Segm n),(Segm k); :: thesis: ( f is onto & f is "increasing & n = k implies f = id n )

assume that

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

A2: n = k ; :: thesis: f = id n

f = id n

let f be Function of (Segm n),(Segm k); :: thesis: ( f is onto & f is "increasing & n = k implies f = id n )

assume that

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

A2: n = k ; :: thesis: f = id n

now :: thesis: f = id nend;

hence
f = id n
; :: thesis: verumper cases
( n = 0 or n > 0 )
;

end;

suppose A4:
n > 0
; :: thesis: f = id n

hence f = id n by A5, FUNCT_1:17; :: thesis: verum

end;

A5: now :: thesis: for m9 being object st m9 in Segm n holds

f . m9 = m9

dom f = n
by A2, A4, FUNCT_2:def 1;f . m9 = m9

let m9 be object ; :: thesis: ( m9 in Segm n implies f . m9 = m9 )

assume A6: m9 in Segm n ; :: thesis: f . m9 = m9

reconsider m = m9 as Element of NAT by A6;

m in rng f by A1, A2, A6, FUNCT_2:def 3;

then A7: ex x being object st

( x in dom f & f . x = m ) by FUNCT_1:def 3;

m in {m} by TARSKI:def 1;

then reconsider F = f " {m} as non empty Subset of NAT by A7, FUNCT_1:def 7;

A8: m < k by A2, A6, NAT_1:44;

then A9: m <= min* (f " {m}) by A1, Th18;

(n - k) + m = m by A2;

then min* (f " {m}) <= m by A1, A8, Th19;

then A10: min* F = m by A9, XXREAL_0:1;

min* F in F by NAT_1:def 1;

then f . m in {m} by A10, FUNCT_1:def 7;

hence f . m9 = m9 by TARSKI:def 1; :: thesis: verum

end;assume A6: m9 in Segm n ; :: thesis: f . m9 = m9

reconsider m = m9 as Element of NAT by A6;

m in rng f by A1, A2, A6, FUNCT_2:def 3;

then A7: ex x being object st

( x in dom f & f . x = m ) by FUNCT_1:def 3;

m in {m} by TARSKI:def 1;

then reconsider F = f " {m} as non empty Subset of NAT by A7, FUNCT_1:def 7;

A8: m < k by A2, A6, NAT_1:44;

then A9: m <= min* (f " {m}) by A1, Th18;

(n - k) + m = m by A2;

then min* (f " {m}) <= m by A1, A8, Th19;

then A10: min* F = m by A9, XXREAL_0:1;

min* F in F by NAT_1:def 1;

then f . m in {m} by A10, FUNCT_1:def 7;

hence f . m9 = m9 by TARSKI:def 1; :: thesis: verum

hence f = id n by A5, FUNCT_1:17; :: thesis: verum