let k, n be Nat; for f being Function of (Segm (n + 1)),(Segm k)
for g being Function of (Segm n),(Segm 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 (Segm (n + 1)),(Segm k); for g being Function of (Segm n),(Segm 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 (Segm n),(Segm k); ( 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
; ( g is onto & g is "increasing )
now ( g is onto & g is "increasing )per cases
( k = 0 or k > 0 )
;
suppose A4:
k > 0
;
( g is onto & g is "increasing )A5:
rng f = k
by A1, FUNCT_2:def 3;
now ( g is onto & g is "increasing )
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
let k1 be
object ;
TARSKI:def 3 ( not k1 in k or k1 in rng g )
assume A8:
k1 in k
;
k1 in rng g
consider x being
object such that A9:
x in dom f
and A10:
f . x = k1
by A5, A8, FUNCT_1:def 3;
dom f = n + 1
by A8, FUNCT_2:def 1;
then reconsider x =
x as
Element of
NAT by A9;
x < n + 1
by A9, NAT_1:44;
then A11:
x <= n
by NAT_1:13;
now k1 in rng gper cases
( x < n or x = n )
by A11, XXREAL_0:1;
suppose
x = n
;
k1 in rng gthen consider m being
Nat such that A15:
m in f " {k1}
and A16:
m <> n
by A2, A4, A10, Th35;
f . m in {k1}
by A15, FUNCT_1:def 7;
then A17:
f . m = k1
by TARSKI:def 1;
m in dom f
by A15, FUNCT_1:def 7;
then
m < n + 1
by NAT_1:44;
then
m <= n
by NAT_1:13;
then
m < n
by A16, XXREAL_0:1;
then A18:
m in Segm n
by NAT_1:44;
A19:
n = dom g
by A4, FUNCT_2:def 1;
then
g . m = f . m
by A3, A18, FUNCT_1:47;
hence
k1 in rng g
by A18, A19, A17, FUNCT_1:def 3;
verum end; end; end;
hence
k1 in rng g
;
verum
end; then A20:
rng g = k
;
(
n = 0 iff
k = 0 )
by A4, A7;
hence
(
g is
onto &
g is
"increasing )
by A20, A6, FUNCT_2:def 3;
verum end; hence
(
g is
onto &
g is
"increasing )
;
verum end; end; end;
hence
( g is onto & g is "increasing )
; verum