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 )

then ( k > 0 & n < n + 1 ) by NAT_1:13;
then ( dom f = n + 1 & n in n + 1 ) by FUNCT_2:def 1, NAT_1:45;
then A5: ( f . n in rng f & rng f = k ) by A1, FUNCT_1:def 5, FUNCT_2:def 3;

now

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

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

then ( dom f = 1 & 1 = {0 } ) by A4, CARD_1:87, FUNCT_2:def 1;
then ( f . 0 in rng f & {(f . 0 )} = k & card k = k & card {(f . 0 )} = 1 ) by A5, CARD_1:50, CARD_1:def 5, FUNCT_1:14;
then A7: ( k = 1 & f " {(f . 0 )} <> {} ) by FUNCT_1:142;

now

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

end;

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

end;

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

k c= rng g

proof

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

now

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

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

then ( x in n & dom g = n ) by A4, FUNCT_2:def 1, NAT_1:45;
then ( x in dom g & g . x = f . x ) by A3, FUNCT_1:70;
hence k1 in rng g by A11, FUNCT_1:def 5; :: thesis: verum

end;

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

then consider m being Element of NAT such that
A13: ( m in f " {k1} & m <> n ) by A2, A4, A11, Th35;
m in dom f by A13, FUNCT_1:def 13;
then m < n + 1 by NAT_1:45;
then m <= n by NAT_1:13;
then m < n by A13, XXREAL_0:1;
then ( m in n & n = dom g & f . m in {k1} ) by A4, A13, FUNCT_1:def 13, FUNCT_2:def 1, NAT_1:45;
then ( m in dom g & g . m = f . m & f . m = k1 ) by A3, FUNCT_1:70, TARSKI:def 1;
hence k1 in rng g by FUNCT_1:def 5; :: thesis: verum

end;

end;

end;

hence k1 in rng g ; :: thesis: verum

end;

then ( rng g = k & k = k + 0 ) by XBOOLE_0:def 10;
then ( g is onto & ( n = 0 implies k = 0 ) & ( k = 0 implies n = 0 ) & ( 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, A4, Th36, FUNCT_2:def 3;
hence ( g is onto & g is "increasing ) by Def1; :: 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