let FT be non empty RelStr ; for g being FinSequence of FT
for A being non empty Subset of FT
for x1, x2 being Element of FT
for B0 being Subset of (FT | A) st g is_minimum_path_in A,x1,x2 & FT is filled & FT is symmetric & B0 = {x1} holds
for i being Element of NAT st i < len g holds
( g . (i + 1) in Finf (B0,i) & ( i >= 1 implies not g . (i + 1) in Finf (B0,(i -' 1)) ) )
let g be FinSequence of FT; for A being non empty Subset of FT
for x1, x2 being Element of FT
for B0 being Subset of (FT | A) st g is_minimum_path_in A,x1,x2 & FT is filled & FT is symmetric & B0 = {x1} holds
for i being Element of NAT st i < len g holds
( g . (i + 1) in Finf (B0,i) & ( i >= 1 implies not g . (i + 1) in Finf (B0,(i -' 1)) ) )
let A be non empty Subset of FT; for x1, x2 being Element of FT
for B0 being Subset of (FT | A) st g is_minimum_path_in A,x1,x2 & FT is filled & FT is symmetric & B0 = {x1} holds
for i being Element of NAT st i < len g holds
( g . (i + 1) in Finf (B0,i) & ( i >= 1 implies not g . (i + 1) in Finf (B0,(i -' 1)) ) )
let x1, x2 be Element of FT; for B0 being Subset of (FT | A) st g is_minimum_path_in A,x1,x2 & FT is filled & FT is symmetric & B0 = {x1} holds
for i being Element of NAT st i < len g holds
( g . (i + 1) in Finf (B0,i) & ( i >= 1 implies not g . (i + 1) in Finf (B0,(i -' 1)) ) )
let B0 be Subset of (FT | A); ( g is_minimum_path_in A,x1,x2 & FT is filled & FT is symmetric & B0 = {x1} implies for i being Element of NAT st i < len g holds
( g . (i + 1) in Finf (B0,i) & ( i >= 1 implies not g . (i + 1) in Finf (B0,(i -' 1)) ) ) )
assume that
A1:
g is_minimum_path_in A,x1,x2
and
A2:
( FT is filled & FT is symmetric )
and
A3:
B0 = {x1}
; for i being Element of NAT st i < len g holds
( g . (i + 1) in Finf (B0,i) & ( i >= 1 implies not g . (i + 1) in Finf (B0,(i -' 1)) ) )
A4:
rng g c= A
by A1;
defpred S1[ Nat] means ( $1 + 1 <= len g implies ( g . ($1 + 1) in Finf (B0,$1) & ( $1 >= 1 implies not g . ($1 + 1) in Finf (B0,($1 -' 1)) ) ) );
defpred S2[ Nat] means for y being Element of FT st y in Finf (B0,$1) holds
ex h being FinSequence of FT st
( h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = y & len h <= $1 + 1 );
A5:
[#] (FT | A) = A
by Def3;
A6:
for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be
Nat;
( S2[k] implies S2[k + 1] )
assume A7:
S2[
k]
;
S2[k + 1]
for
y being
Element of
FT st
y in Finf (
B0,
(k + 1)) holds
ex
h being
FinSequence of
FT st
(
h is
continuous &
rng h c= A &
h . 1
= x1 &
h . (len h) = y &
len h <= (k + 1) + 1 )
proof
let y be
Element of
FT;
( y in Finf (B0,(k + 1)) implies ex h being FinSequence of FT st
( h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = y & len h <= (k + 1) + 1 ) )
A8:
Finf (
B0,
(k + 1))
= (Finf (B0,k)) ^f
by FINTOPO3:31;
assume
y in Finf (
B0,
(k + 1))
;
ex h being FinSequence of FT st
( h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = y & len h <= (k + 1) + 1 )
then consider x being
Element of
(FT | A) such that A9:
x = y
and A10:
ex
y2 being
Element of
(FT | A) st
(
y2 in Finf (
B0,
k) &
x in U_FT y2 )
by A8;
A11:
[#] (FT | A) = A
by Def3;
then A12:
{y} c= A
by A9, ZFMISC_1:31;
consider y2 being
Element of
(FT | A) such that A13:
y2 in Finf (
B0,
k)
and A14:
x in U_FT y2
by A10;
y2 in the
carrier of
(FT | A)
;
then reconsider y3 =
y2 as
Element of
FT by A11;
consider h2 being
FinSequence of
FT such that A15:
h2 is
continuous
and A16:
rng h2 c= A
and A17:
h2 . 1
= x1
and A18:
h2 . (len h2) = y3
and A19:
len h2 <= k + 1
by A7, A13;
U_FT y2 = (U_FT y3) /\ A
by A11, Def2;
then A20:
y in U_FT y3
by A9, A14, XBOOLE_0:def 4;
reconsider h3 =
h2 ^ <*y*> as
FinSequence of
FT ;
(
rng (h2 ^ <*y*>) = (rng h2) \/ (rng <*y*>) &
rng <*y*> = {y} )
by FINSEQ_1:31, FINSEQ_1:39;
then A21:
rng h3 c= A
by A16, A12, XBOOLE_1:8;
1
<= len h2
by A15;
then
1
in dom h2
by FINSEQ_3:25;
then A22:
h3 . 1
= x1
by A17, FINSEQ_1:def 7;
len <*y*> = 1
by FINSEQ_1:40;
then A23:
len h3 = (len h2) + 1
by FINSEQ_1:22;
then A24:
h3 . (len h3) = y
by FINSEQ_1:42;
len h3 <= (k + 1) + 1
by A19, A23, XREAL_1:6;
hence
ex
h being
FinSequence of
FT st
(
h is
continuous &
rng h c= A &
h . 1
= x1 &
h . (len h) = y &
len h <= (k + 1) + 1 )
by A15, A18, A20, A21, A22, A24, Th43;
verum
end;
hence
S2[
k + 1]
;
verum
end;
A25:
g . 1 = x1
by A1;
then A26:
g . 1 in {x1}
by TARSKI:def 1;
A27:
g . (len g) = x2
by A1;
A28:
g is continuous
by A1;
then
1 <= len g
;
then
1 in dom g
by FINSEQ_3:25;
then
x1 in rng g
by A25, FUNCT_1:def 3;
then A29:
{x1} c= A
by A4, ZFMISC_1:31;
for y being Element of FT st y in Finf (B0,0) holds
ex h being FinSequence of FT st
( h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = y & len h <= 0 + 1 )
then A32:
S2[ 0 ]
;
A33:
for k being Nat holds S2[k]
from NAT_1:sch 2(A32, A6);
A34:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A35:
S1[
k]
;
S1[k + 1]
per cases
( (k + 1) + 1 > len g or (k + 1) + 1 <= len g )
;
suppose A36:
(k + 1) + 1
<= len g
;
S1[k + 1]A37:
1
<= k + 1
by NAT_1:12;
then
1
< (k + 1) + 1
by NAT_1:13;
then
(k + 1) + 1
in dom g
by A36, FINSEQ_3:25;
then A38:
g . ((k + 1) + 1) in rng g
by FUNCT_1:def 3;
reconsider y0 =
g . (k + 1) as
Element of
(FT | A) by A35, A36, NAT_1:13;
A39:
k + 1
< len g
by A36, NAT_1:13;
then
k + 1
in dom g
by A37, FINSEQ_3:25;
then A40:
g . (k + 1) = g /. (k + 1)
by PARTFUN1:def 6;
1
< (k + 1) + 1
by A37, NAT_1:13;
then A41:
(k + 1) + 1
in dom g
by A36, FINSEQ_3:25;
A42:
now not g . ((k + 1) + 1) in Finf (B0,k)assume A43:
g . ((k + 1) + 1) in Finf (
B0,
k)
;
contradictionthen consider x being
Element of
(FT | A) such that A45:
g . ((k + 1) + 1) = x
and
ex
y being
Element of
(FT | A) st
(
y in Finf (
B0,
(k -' 1)) &
x in U_FT y )
;
x in A
by A5;
then reconsider x3 =
x as
Element of
FT ;
consider h being
FinSequence of
FT such that A46:
h is
continuous
and A47:
rng h c= A
and A48:
h . 1
= x1
and A49:
h . (len h) = x3
and A50:
len h <= k + 1
by A33, A43, A45;
reconsider s =
h ^ (g /^ ((k + 1) + 1)) as
FinSequence of
FT ;
A51:
len s = (len h) + (len (g /^ ((k + 1) + 1)))
by FINSEQ_1:22;
g = (g | ((k + 1) + 1)) ^ (g /^ ((k + 1) + 1))
by RFINSEQ:8;
then A52:
len g = (len (g | ((k + 1) + 1))) + (len (g /^ ((k + 1) + 1)))
by FINSEQ_1:22;
A53:
1
<= len h
by A46;
then
len h in dom h
by FINSEQ_3:25;
then A54:
h . (len h) = h /. (len h)
by PARTFUN1:def 6;
len (g | ((k + 1) + 1)) = (k + 1) + 1
by A36, FINSEQ_1:59;
then A55:
len (g | ((k + 1) + 1)) > len h
by A50, NAT_1:13;
then A56:
len s < len g
by A51, A52, XREAL_1:8;
per cases
( (k + 1) + 1 < len g or (k + 1) + 1 >= len g )
;
suppose A57:
(k + 1) + 1
< len g
;
contradictionthen
len g >= 1
+ ((k + 1) + 1)
by NAT_1:13;
then
1
<= (len g) - ((k + 1) + 1)
by XREAL_1:19;
then
1
<= len (g /^ ((k + 1) + 1))
by A57, RFINSEQ:def 1;
then A58:
1
in dom (g /^ ((k + 1) + 1))
by FINSEQ_3:25;
A59:
g . ((k + 1) + 1) = g /. ((k + 1) + 1)
by A41, PARTFUN1:def 6;
A60:
g /^ ((k + 1) + 1) is
continuous
by A28, A57, Th47;
then
1
<= len (g /^ ((k + 1) + 1))
;
then
len (g /^ ((k + 1) + 1)) in dom (g /^ ((k + 1) + 1))
by FINSEQ_3:25;
then A61:
s . (len s) =
(g /^ ((k + 1) + 1)) . (len (g /^ ((k + 1) + 1)))
by A51, FINSEQ_1:def 7
.=
x2
by A27, A57, FINSEQ_6:185
;
1
<= (k + 1) + 1
by NAT_1:12;
then
g . (((k + 1) + 1) + 1) in U_FT (g /. ((k + 1) + 1))
by A28, A57, A59;
then
(g /^ ((k + 1) + 1)) . 1
in U_FT (h /. (len h))
by A45, A49, A54, A57, A59, A58, RFINSEQ:def 1;
then A62:
s is
continuous
by A46, A60, Th44;
1
in dom h
by A53, FINSEQ_3:25;
then A63:
s . 1
= x1
by A48, FINSEQ_1:def 7;
rng (g /^ ((k + 1) + 1)) c= rng g
by FINSEQ_5:33;
then A64:
rng (g /^ ((k + 1) + 1)) c= A
by A4;
rng s = (rng h) \/ (rng (g /^ ((k + 1) + 1)))
by FINSEQ_1:31;
then
rng s c= A
by A47, A64, XBOOLE_1:8;
hence
contradiction
by A1, A56, A62, A63, A61;
verum end; suppose A65:
(k + 1) + 1
>= len g
;
contradictionthen
g /^ ((k + 1) + 1) = <*> the
carrier of
FT
by FINSEQ_5:32;
then A66:
s = h
by FINSEQ_1:34;
(k + 1) + 1
= len g
by A36, A65, XXREAL_0:1;
hence
contradiction
by A1, A45, A46, A47, A48, A49, A55, A51, A52, A66;
verum end; end;
[#] (FT | A) = A
by Def3;
then A67:
U_FT y0 = (U_FT (g /. (k + 1))) /\ A
by A40, Def2;
g . ((k + 1) + 1) in U_FT (g /. (k + 1))
by A28, A39, A37, A40;
then
g . ((k + 1) + 1) in U_FT y0
by A4, A67, A38, XBOOLE_0:def 4;
then A68:
g . ((k + 1) + 1) in (Finf (B0,k)) ^f
by A35, A36, NAT_1:13;
(k + 1) -' 1 =
(k + 1) - 1
by NAT_D:37
.=
k
;
hence
S1[
k + 1]
by A68, A42, FINTOPO3:31;
verum end;
end;
let i be Element of NAT ; ( i < len g implies ( g . (i + 1) in Finf (B0,i) & ( i >= 1 implies not g . (i + 1) in Finf (B0,(i -' 1)) ) ) )
assume
i < len g
; ( g . (i + 1) in Finf (B0,i) & ( i >= 1 implies not g . (i + 1) in Finf (B0,(i -' 1)) ) )
then A69:
i + 1 <= len g
by NAT_1:13;
Finf ({x1},0) =
{x1}
by FINTOPO3:32
.=
Finf (B0,0)
by A3, FINTOPO3:32
;
then A70:
S1[ 0 ]
by A26, FINTOPO3:32;
for j being Nat holds S1[j]
from NAT_1:sch 2(A70, A34);
hence
( g . (i + 1) in Finf (B0,i) & ( i >= 1 implies not g . (i + 1) in Finf (B0,(i -' 1)) ) )
by A69; verum