let n, k be Element of 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 )

n < n + 1 by NAT_1:13;
then A5: n in n + 1 by NAT_1:45;
A6: rng f = k by A1, FUNCT_2:def 3;
dom f = n + 1 by A4, FUNCT_2:def 1;
then A7: f . n in rng f by A5, FUNCT_1:def 5;

now

per cases ( n = 0 or n > 0 ) ;

suppose A8: n = 0 ; :: thesis: ( g is onto & g is "increasing )

now

let x be set ; :: thesis: ( x in f " {(f . 0 )} implies x in {0 } )
assume x in f " {(f . 0 )} ; :: thesis: x in {0 }
then x in dom f by FUNCT_1:def 13;
hence x in {0 } by A8, CARD_1:87; :: thesis: verum

end;

then A9: f " {(f . 0 )} c= {0 } by TARSKI:def 3;
f " {(f . 0 )} <> {} by A7, A6, FUNCT_1:142;
hence ( g is onto & g is "increasing ) by A2, A8, A9, ZFMISC_1:39; :: thesis: verum

end;

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

k = k + 0 ;
then A10: for i, j being Element of NAT st i in rng g & j in rng g & i < j holds
min* (g " {i}) < min* (g " {j}) by A1, A3, Th36;
A11: k c= rng g

proof

A12: 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 A13: k1 in k ; :: thesis: k1 in rng g
consider x being set such that
A14: x in dom f and
A15: f . x = k1 by A6, A13, FUNCT_1:def 5;
dom f = n + 1 by A13, FUNCT_2:def 1;
then reconsider x = x as Element of NAT by A14, A12;
x < n + 1 by A14, NAT_1:45;
then A16: x <= n by NAT_1:13;

now

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

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

A18: dom g = n by A4, FUNCT_2:def 1;
A19: x in n by A17, NAT_1:45;
then g . x = f . x by A3, A18, FUNCT_1:70;
hence k1 in rng g by A15, A19, A18, FUNCT_1:def 5; :: thesis: verum

end;

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

then consider m being Element of NAT such that
A20: m in f " {k1} and
A21: m <> n by A2, A4, A15, Th35;
f . m in {k1} by A20, FUNCT_1:def 13;
then A22: f . m = k1 by TARSKI:def 1;
m in dom f by A20, FUNCT_1:def 13;
then m < n + 1 by NAT_1:45;
then m <= n by NAT_1:13;
then m < n by A21, XXREAL_0:1;
then A23: m in n by NAT_1:45;
A24: n = dom g by A4, FUNCT_2:def 1;
then g . m = f . m by A3, A23, FUNCT_1:70;
hence k1 in rng g by A23, A24, A22, FUNCT_1:def 5; :: thesis: verum

end;

end;

end;

hence k1 in rng g ; :: thesis: verum

end;

then A25: rng g = k by XBOOLE_0:def 10;
( n = 0 iff k = 0 ) by A4, A11;
hence ( g is onto & g is "increasing ) by A25, A10, Def1, FUNCT_2:def 3; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

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