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 )
now :: thesis: ( g is onto & g is "increasing )
per cases ( k = 0 or k > 0 ) ;
suppose k = 0 ; :: thesis: ( g is onto & g is "increasing )
hence ( g is onto & g is "increasing ) by A1; :: thesis: verum
end;
suppose A4: k > 0 ; :: thesis: ( g is onto & g is "increasing )
A5: rng f = k by ;
now :: thesis: ( g is onto & g is "increasing )
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
proof
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 ;
dom f = n + 1 by ;
then reconsider x = x as Element of NAT by A9;
x < n + 1 by ;
then A11: x <= n by NAT_1:13;
now :: thesis: k1 in rng g
per cases ( x < n or x = n ) by ;
suppose A12: x < n ; :: thesis: k1 in rng g
A13: dom g = n by ;
A14: x in Segm n by ;
then g . x = f . x by ;
hence k1 in rng g by ; :: thesis: verum
end;
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 ;
then A17: f . m = k1 by TARSKI:def 1;
m in dom f by ;
then m < n + 1 by NAT_1:44;
then m <= n by NAT_1:13;
then m < n by ;
then A18: m in Segm n by NAT_1:44;
A19: n = dom g by ;
then g . m = f . m by ;
hence k1 in rng g by ; :: thesis: verum
end;
end;
end;
hence k1 in rng g ; :: thesis: verum
end;
then A20: rng g = k ;
( n = 0 iff k = 0 ) by A4, A7;
hence ( g is onto & g is "increasing ) by ; :: thesis: verum
end;
hence ( g is onto & g is "increasing ) ; :: thesis: verum
end;
end;
end;
hence ( g is onto & g is "increasing ) ; :: thesis: verum