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 A1, FUNCT_2:def 3;

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 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 g

per cases ( x < n or x = n ) by A11, XXREAL_0:1;

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;

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;

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 A20, A6, FUNCT_2:def 3; :: thesis: verum

end;

hence ( g is onto & g is "increasing ) ; :: thesis: verum

end;

end;

end;

hence ( g is onto & g is "increasing ) ; :: thesis: verum