let n, k be Nat; :: thesis: for f being Function of (n + 1),k
for g being Function of n,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 (n + 1),k; :: thesis: for g being Function of n,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 n,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

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, Def1; :: 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

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

A8: n + 1 is Subset of NAT by Th8;
let k1 be set ; :: according to TARSKI:def 3 :: thesis: ( not k1 in k or k1 in rng g )
assume A9: k1 in k ; :: thesis: k1 in rng g
consider x being set such that
A10: x in dom f and
A11: f . x = k1 by A5, A9, FUNCT_1:def 3;
dom f = n + 1 by A9, FUNCT_2:def 1;
then reconsider x = x as Element of NAT by A10, A8;
x < n + 1 by A10, NAT_1:44;
then A12: x <= n by NAT_1:13;

now

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

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

A14: dom g = n by A4, FUNCT_2:def 1;
A15: x in n by A13, NAT_1:44;
then g . x = f . x by A3, A14, FUNCT_1:47;
hence k1 in rng g by A11, A15, A14, FUNCT_1:def 3; :: thesis: verum

end;

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

then consider m being Nat such that
A16: m in f " {k1} and
A17: m <> n by A2, A4, A11, Th35;
f . m in {k1} by A16, FUNCT_1:def 7;
then A18: f . m = k1 by TARSKI:def 1;
m in dom f by A16, FUNCT_1:def 7;
then m < n + 1 by NAT_1:44;
then m <= n by NAT_1:13;
then m < n by A17, XXREAL_0:1;
then A19: m in n by NAT_1:44;
A20: n = dom g by A4, FUNCT_2:def 1;
then g . m = f . m by A3, A19, FUNCT_1:47;
hence k1 in rng g by A19, A20, A18, FUNCT_1:def 3; :: thesis: verum

end;

end;

end;

hence k1 in rng g ; :: thesis: verum

end;

then A21: rng g = k by XBOOLE_0:def 10;
( n = 0 iff k = 0 ) by A4, A7;
hence ( g is onto & g is "increasing ) by A21, A6, Def1, 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