let k, n be Nat; for f being Function of (Segm (n + 1)),(Segm (k + 1)) st f is onto & f is "increasing & f " {(f . n)} = {n} holds
( rng (f | n) c= Segm k & ( for g being Function of (Segm n),(Segm k) st g = f | n holds
( g is onto & g is "increasing ) ) )
let f be Function of (Segm (n + 1)),(Segm (k + 1)); ( f is onto & f is "increasing & f " {(f . n)} = {n} implies ( rng (f | n) c= Segm k & ( for g being Function of (Segm n),(Segm k) st g = f | n holds
( g is onto & g is "increasing ) ) ) )
assume that
A1:
( f is onto & f is "increasing )
and
A2:
f " {(f . n)} = {n}
; ( rng (f | n) c= Segm k & ( for g being Function of (Segm n),(Segm k) st g = f | n holds
( g is onto & g is "increasing ) ) )
now ( rng (f | n) c= Segm k & ( for g being Function of (Segm n),(Segm k) st g = f | n holds
( g is onto & g is "increasing ) ) )per cases
( n = 0 or n > 0 )
;
suppose A4:
n > 0
;
( rng (f | n) c= Segm k & ( for g being Function of (Segm n),(Segm k) st g = f | n holds
( g is onto & g is "increasing ) ) )thus A5:
rng (f | n) c= Segm k
for g being Function of (Segm n),(Segm k) st g = f | n holds
( g is onto & g is "increasing )proof
let fi be
object ;
TARSKI:def 3 ( not fi in rng (f | n) or fi in Segm k )
assume A6:
fi in rng (f | n)
;
fi in Segm k
rng (f | n) c= rng f
by RELAT_1:70;
then
fi in rng f
by A6;
then A7:
fi in k + 1
;
k + 1 is
Subset of
NAT
by Th8;
then reconsider fi =
fi as
Element of
NAT by A7;
consider i being
object such that A8:
i in dom (f | n)
and A9:
(f | n) . i = fi
by A6, FUNCT_1:def 3;
i in (dom f) /\ n
by A8, RELAT_1:61;
then A10:
i in n
by XBOOLE_0:def 4;
n is
Subset of
NAT
by Th8;
then reconsider i =
i as
Element of
NAT by A10;
A11:
f . i < k
proof
f . i < k + 1
by NAT_1:44;
then A12:
f . i <= k
by NAT_1:13;
assume
f . i >= k
;
contradiction
then A13:
f . i = k
by A12, XXREAL_0:1;
A14:
f . i in {(f . i)}
by TARSKI:def 1;
A15:
f . n = k
by A1, A2, Th34;
A16:
i in (dom f) /\ n
by A8, RELAT_1:61;
then
i in dom f
by XBOOLE_0:def 4;
then
i in f " {(f . n)}
by A13, A14, A15, FUNCT_1:def 7;
then
(
i >= min* (f " {(f . n)}) &
i in NAT &
n in NAT )
by NAT_1:def 1, ORDINAL1:def 12;
then A17:
i >= n
by A2, Th5;
i in Segm n
by A16, XBOOLE_0:def 4;
hence
contradiction
by A17, NAT_1:44;
verum
end;
f . i = (f | n) . i
by A8, FUNCT_1:47;
hence
fi in Segm k
by A9, A11, NAT_1:44;
verum
end; thus
for
g being
Function of
(Segm n),
(Segm k) st
g = f | n holds
(
g is
onto &
g is
"increasing )
verumproof
let g be
Function of
(Segm n),
(Segm k);
( g = f | n implies ( g is onto & g is "increasing ) )
assume A18:
g = f | n
;
( g is onto & g is "increasing )
Segm k c= rng g
proof
n < n + 1
by NAT_1:13;
then A19:
Segm n c= Segm (n + 1)
by NAT_1:39;
dom f = n + 1
by FUNCT_2:def 1;
then A20:
n = (dom f) /\ n
by A19, XBOOLE_1:28;
let k1 be
object ;
TARSKI:def 3 ( not k1 in Segm k or k1 in rng g )
assume A21:
k1 in Segm k
;
k1 in rng g
reconsider k9 =
k1 as
Element of
NAT by A21;
k9 < k
by A21, NAT_1:44;
then
k9 < k + 1
by NAT_1:13;
then A22:
k9 in Segm (k + 1)
by NAT_1:44;
A23:
dom f = n + 1
by FUNCT_2:def 1;
rng f = k + 1
by A1, FUNCT_2:def 3;
then consider n1 being
object such that A24:
n1 in dom f
and A25:
f . n1 = k9
by A22, FUNCT_1:def 3;
reconsider n1 =
n1 as
Element of
NAT by A24, A23;
n1 < n + 1
by A24, NAT_1:44;
then A26:
n1 <= n
by NAT_1:13;
reconsider nn =
k1 as
set by TARSKI:1;
A:
not
nn in nn
;
f . n = k
by A1, A2, Th34;
then
n1 <> n
by A, A21, A25;
then A27:
n1 < n
by A26, XXREAL_0:1;
(dom f) /\ n = dom (f | n)
by RELAT_1:61;
then A28:
n1 in dom g
by A18, A27, A20, NAT_1:44;
then
g . n1 in rng g
by FUNCT_1:def 3;
hence
k1 in rng g
by A18, A25, A28, FUNCT_1:47;
verum
end;
then
k = rng g
;
hence
g is
onto
by FUNCT_2:def 3;
g is "increasing
A29:
(dom f) /\ n = dom (f | n)
by RELAT_1:61;
n < n + 1
by NAT_1:13;
then A30:
Segm n c= Segm (n + 1)
by NAT_1:39;
dom f = n + 1
by FUNCT_2:def 1;
then A31:
n = (dom f) /\ n
by A30, XBOOLE_1:28;
0 in Segm n
by A4, NAT_1:44;
then
(f | n) . 0 in rng (f | n)
by A31, A29, FUNCT_1:def 3;
then A32:
(
n = 0 iff
k = 0 )
by A5;
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, A18, Th36;
hence
g is
"increasing
by A32;
verum
end; end;
hence
( rng (f | n) c= Segm k & ( for g being Function of (Segm n),(Segm k) st g = f | n holds
( g is onto & g is "increasing ) ) )
; verum