let n, k be Element of NAT ; :: thesis: for f being Function of (n + 1),(k + 1) st f is onto & f is "increasing & f " {(f . n)} = {n} holds
( rng (f | n) c= k & ( for g being Function of n,k st g = f | n holds
( g is onto & g is "increasing ) ) )
let f be Function of (n + 1),(k + 1); :: thesis: ( f is onto & f is "increasing & f " {(f . n)} = {n} implies ( rng (f | n) c= k & ( for g being Function of n,k st g = f | n holds
( g is onto & g is "increasing ) ) ) )
assume A1: ( f is onto & f is "increasing & f " {(f . n)} = {n} ) ; :: thesis: ( rng (f | n) c= k & ( for g being Function of n,k st g = f | n holds
( g is onto & g is "increasing ) ) )

now

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

suppose A2: n = 0 ; :: thesis: ( rng (f | n) c= k & ( for g being Function of n,k st g = f | n holds
( g is onto & g is "increasing ) ) )

then ( 0 + 1 >= k + 1 & dom (f | n) = (dom f) /\ 0 ) by A1, Th17;
then ( k = 0 & rng (f | n) = 0 ) by RELAT_1:65, XREAL_1:8;
hence ( rng (f | n) c= k & ( for g being Function of n,k st g = f | n holds
( g is onto & g is "increasing ) ) ) by A2, Th15; :: thesis: verum

end;

suppose A3: n > 0 ; :: thesis: ( rng (f | n) c= k & ( for g being Function of n,k st g = f | n holds
( g is onto & g is "increasing ) ) )

thus A4: rng (f | n) c= k :: thesis: for g being Function of n,k st g = f | n holds
( g is onto & g is "increasing )

proof

let fi be set ; :: according to TARSKI:def 3 :: thesis: ( not fi in rng (f | n) or fi in k )
assume A5: fi in rng (f | n) ; :: thesis: fi in k
( fi in k + 1 & k + 1 is Subset of NAT ) by A5, Th8;
then reconsider fi = fi as Element of NAT ;
consider i being set such that
A6: ( i in dom (f | n) & (f | n) . i = fi ) by A5, FUNCT_1:def 5;
i in (dom f) /\ n by A6, RELAT_1:90;
then ( i in n & n is Subset of NAT ) by Th8, XBOOLE_0:def 4;
then reconsider i = i as Element of NAT ;
f . i < k

proof

assume A7: f . i >= k ; :: thesis: contradiction
i in (dom f) /\ n by A6, RELAT_1:90;
then A8: ( i in dom f & f . i < k + 1 & i in n ) by NAT_1:45, XBOOLE_0:def 4;
then f . i <= k by NAT_1:13;
then ( f . i = k & f . i in {(f . i)} & f . n = k ) by A1, A7, Th34, TARSKI:def 1, XXREAL_0:1;
then i in f " {(f . n)} by A8, FUNCT_1:def 13;
then i >= min* (f " {(f . n)}) by NAT_1:def 1;
then i >= n by A1, Th5;
hence contradiction by A8, NAT_1:45; :: thesis: verum

end;

then ( f . i = (f | n) . i & f . i in k ) by A6, FUNCT_1:70, NAT_1:45;
hence fi in k by A6; :: thesis: verum

end;

thus for g being Function of n,k st g = f | n holds
( g is onto & g is "increasing ) :: thesis: verum

proof

let g be Function of n,k; :: thesis: ( g = f | n implies ( g is onto & g is "increasing ) )
assume A9: g = f | n ; :: thesis: ( g is onto & g is "increasing )
thus g is onto :: thesis: g is "increasing

proof

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
k is Subset of NAT by Th8;
then reconsider k' = k1 as Element of NAT by A10;
k' < k by A10, NAT_1:45;
then k' < k + 1 by NAT_1:13;
then ( k' in k + 1 & rng f = k + 1 ) by A1, FUNCT_2:def 3, NAT_1:45;
then consider n1 being set such that
A11: ( n1 in dom f & f . n1 = k' ) by FUNCT_1:def 5;
( dom f = n + 1 & n + 1 is Subset of NAT ) by Th8, FUNCT_2:def 1;
then reconsider n1 = n1 as Element of NAT by A11;
( n1 < n + 1 & f . n = k & n < n + 1 ) by A1, A11, Th34, NAT_1:13, NAT_1:45;
then ( n1 <= n & n1 <> n & n c= n + 1 & dom f = n + 1 ) by A10, A11, FUNCT_2:def 1, NAT_1:13, NAT_1:40;
then ( n1 < n & n = (dom f) /\ n & (dom f) /\ n = dom (f | n) ) by RELAT_1:90, XBOOLE_1:28, XXREAL_0:1;
then n1 in dom g by A9, NAT_1:45;
then ( g . n1 in rng g & g . n1 = f . n1 ) by A9, FUNCT_1:70, FUNCT_1:def 5;
hence k1 in rng g by A11; :: thesis: verum

end;

then k = rng g by XBOOLE_0:def 10;
hence g is onto by FUNCT_2:def 3; :: thesis: verum

end;

thus g is "increasing :: thesis: verum

proof

( n = 0 iff k = 0 )

proof

n < n + 1 by NAT_1:13;
then ( n c= n + 1 & dom f = n + 1 ) by FUNCT_2:def 1, NAT_1:40;
then ( n = (dom f) /\ n & (dom f) /\ n = dom (f | n) & 0 in n ) by A3, NAT_1:45, RELAT_1:90, XBOOLE_1:28;
then (f | n) . 0 in rng (f | n) by FUNCT_1:def 5;
hence ( n = 0 iff k = 0 ) by A4; :: thesis: verum

end;

then ( ( 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, A9, Th36;
hence g is "increasing by Def1; :: thesis: verum

end;

end;

end;

end;

end;

hence ( rng (f | n) c= k & ( for g being Function of n,k st g = f | n holds
( g is onto & g is "increasing ) ) ) ; :: thesis: verum