let FT be non empty RelStr ; :: thesis:
let g be FinSequence of FT; :: thesis:
let A be non empty Subset of FT; :: thesis:
let x1, x2 be Element of FT; :: thesis:
let B0 be Subset of (FT | A); :: thesis:
assume A1: ( g is_minimum_path_in A,x1,x2 & FT is reflexive & FT is symmetric & x1 <> x2 & B0 = {x1} ) ; :: thesis:
then A2: ( g is continuous & rng g c= A & g . 1 = x1 & g . (len g) = x2 & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds
len g <= len h ) ) by Def8;
then 1 <= len g by Def6;
then 1 in dom g by FINSEQ_3:27;
then A3: x1 in rng g by A2, FUNCT_1:def 5;
A4: FT | A is reflexive by A1;
A5: [#] (FT | A) = A by Def3;
A6: {x1} c= A by A2, A3, ZFMISC_1:37;
let i be Element of NAT ; :: thesis:
assume i < len g ; :: thesis:
then A7: i + 1 <= len g by NAT_1:13;
defpred S₁[ Element of 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 );
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 )

proof

let y be Element of FT; :: thesis:
assume y in Finf B0,0 ; :: thesis:
then y in {x1} by A1, FINTOPO3:32;
then A8: y = x1 by TARSKI:def 1;
A9: rng <*x1*> = {x1} by FINSEQ_1:56;
( <*x1*> . 1 = x1 & len <*x1*> = 1 ) by FINSEQ_1:57;
hence 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 ) by A6, A8, A9; :: thesis:

end;

then A10: S₁[ 0 ] ;
A11: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis:
assume A12: S₁[k] ; :: thesis:
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; :: thesis:
assume A13: y in Finf B0,(k + 1) ; :: thesis:
Finf B0,(k + 1) = (Finf B0,k) ^f by FINTOPO3:31;
then consider x being Element of (FT | A) such that
A14: ( x = y & ex y2 being Element of (FT | A) st
( y2 in Finf B0,k & x in U_FT y2 ) ) by A13;
consider y2 being Element of (FT | A) such that
A15: ( y2 in Finf B0,k & x in U_FT y2 ) by A14;
A16: y2 in the carrier of (FT | A) ;
A17: [#] (FT | A) = A by Def3;
then reconsider y3 = y2 as Element of FT by A16;
consider h2 being FinSequence of FT such that
A18: ( h2 is continuous & rng h2 c= A & h2 . 1 = x1 & h2 . (len h2) = y3 & len h2 <= k + 1 ) by A12, A15;
reconsider h3 = h2 ^ <*y*> as FinSequence of FT ;
A19: ( len <*y*> = 1 & <*y*> . 1 = y ) by FINSEQ_1:57;
U_FT y2 = (U_FT y3) /\ A by A17, Def2;
then A20: y in U_FT y3 by A14, A15, XBOOLE_0:def 4;
A21: rng (h2 ^ <*y*>) = (rng h2) \/ (rng <*y*>) by FINSEQ_1:44;
A22: {y} c= A by A14, A17, ZFMISC_1:37;
rng <*y*> = {y} by FINSEQ_1:56;
then A23: rng h3 c= A by A18, A21, A22, XBOOLE_1:8;
1 <= len h2 by A18, Def6;
then 1 in dom h2 by FINSEQ_3:27;
then A24: h3 . 1 = x1 by A18, FINSEQ_1:def 7;
A25: len h3 = (len h2) + 1 by A19, FINSEQ_1:35;
then A26: len h3 <= (k + 1) + 1 by A18, XREAL_1:8;
h3 . (len h3) = y by A25, FINSEQ_1:59;
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 A18, A20, A23, A24, A26, Th44; :: thesis:

end;

hence S₁[k + 1] ; :: thesis:

end;

A27: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A10, A11);
defpred S₂[ 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) ) ) );
A28: Finf {x1},0 = {x1} by FINTOPO3:32
.= Finf B0,0 by A1, FINTOPO3:32 ;
g . 1 in {x1} by A2, TARSKI:def 1;
then A29: S₂[ 0 ] by A28, FINTOPO3:32;
A30: for k being Element of NAT st S₂[k] holds
S₂[k + 1]

proof

let k be Element of NAT ; :: thesis:
assume A31: S₂[k] ; :: thesis:

per cases ) + 1 > len g or (k + 1) + 1 <= len g ) ;

suppose (k + 1) + 1 > len g ; :: thesis:

hence S₂[k + 1] ; :: thesis:

end;

suppose A32: (k + 1) + 1 <= len g ; :: thesis:

then A33: k + 1 < len g by NAT_1:13;
A34: 1 <= k + 1 by NAT_1:12;
then k + 1 in dom g by A33, FINSEQ_3:27;
then A35: g . (k + 1) = g /. (k + 1) by PARTFUN1:def 8;
reconsider y0 = g . (k + 1) as Element of (FT | A) by A31, A32, NAT_1:13;
[#] (FT | A) = A by Def3;
then A36: U_FT y0 = (U_FT (g /. (k + 1))) /\ A by A35, Def2;
1 < (k + 1) + 1 by A34, NAT_1:13;
then (k + 1) + 1 in dom g by A32, FINSEQ_3:27;
then A37: g . ((k + 1) + 1) in rng g by FUNCT_1:def 5;
g . ((k + 1) + 1) in U_FT (g /. (k + 1)) by A2, A33, A34, A35, Def6;
then A38: g . ((k + 1) + 1) in U_FT y0 by A2, A36, A37, XBOOLE_0:def 4;
1 < (k + 1) + 1 by A34, NAT_1:13;
then A39: (k + 1) + 1 in dom g by A32, FINSEQ_3:27;
A40: g . ((k + 1) + 1) in (Finf B0,k) ^f by A31, A32, A38, NAT_1:13;
A41: (k + 1) -' 1 = (k + 1) - 1 by NAT_D:37
.= k ;

now

assume A42: g . ((k + 1) + 1) in Finf B0,k ; :: thesis:

now

per cases ;

suppose A43: k = 0 ; :: thesis:

then k - 1 < 0 ;
then k -' 1 = 0 by XREAL_0:def 2;
then Finf B0,k c= (Finf B0,(k -' 1)) ^f by A4, A43, FINTOPO3:1;
hence g . ((k + 1) + 1) in (Finf B0,(k -' 1)) ^f by A42; :: thesis:

end;

suppose k > 0 ; :: thesis:

then k >= 0 + 1 by NAT_1:13;
then k = (k -' 1) + 1 by XREAL_1:237;
hence g . ((k + 1) + 1) in (Finf B0,(k -' 1)) ^f by A42, FINTOPO3:31; :: thesis:

end;

then consider x being Element of (FT | A) such that
A44: ( g . ((k + 1) + 1) = x & 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
A45: ( h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x3 & len h <= k + 1 ) by A27, A42, A44;
A46: 1 <= len h by A45, Def6;
then len h in dom h by FINSEQ_3:27;
then A47: h . (len h) = h /. (len h) by PARTFUN1:def 8;
len (g | ((k + 1) + 1)) = (k + 1) + 1 by A32, FINSEQ_1:80;
then A48: len (g | ((k + 1) + 1)) > len h by A45, NAT_1:13;
reconsider s = h ^ (g /^ ((k + 1) + 1)) as FinSequence of FT ;
A49: len s = (len h) + (len (g /^ ((k + 1) + 1))) by FINSEQ_1:35;
g = (g | ((k + 1) + 1)) ^ (g /^ ((k + 1) + 1)) by RFINSEQ:21;
then A50: len g = (len (g | ((k + 1) + 1))) + (len (g /^ ((k + 1) + 1))) by FINSEQ_1:35;
then A51: len s < len g by A48, A49, XREAL_1:10;

per cases ) + 1 < len g or (k + 1) + 1 >= len g ) ;

suppose A52: (k + 1) + 1 < len g ; :: thesis:

A53: 1 <= (k + 1) + 1 by NAT_1:12;
A54: g . ((k + 1) + 1) = g /. ((k + 1) + 1) by A39, PARTFUN1:def 8;
then A55: g . (((k + 1) + 1) + 1) in U_FT (g /. ((k + 1) + 1)) by A2, A52, A53, Def6;
len g >= 1 + ((k + 1) + 1) by A52, NAT_1:13;
then 1 <= (len g) - ((k + 1) + 1) by XREAL_1:21;
then 1 <= len (g /^ ((k + 1) + 1)) by A52, RFINSEQ:def 2;
then 1 in dom (g /^ ((k + 1) + 1)) by FINSEQ_3:27;
then A56: (g /^ ((k + 1) + 1)) . 1 in U_FT (h /. (len h)) by A44, A45, A47, A52, A54, A55, RFINSEQ:def 2;
A57: g /^ ((k + 1) + 1) is continuous by A2, A52, Th48;
then A58: s is continuous by A45, A56, Th45;
A59: 1 <= len (g /^ ((k + 1) + 1)) by A57, Def6;
rng (g /^ ((k + 1) + 1)) c= rng g by FINSEQ_5:36;
then A60: rng (g /^ ((k + 1) + 1)) c= A by A2, XBOOLE_1:1;
rng s = (rng h) \/ (rng (g /^ ((k + 1) + 1))) by FINSEQ_1:44;
then A61: rng s c= A by A45, A60, XBOOLE_1:8;
1 in dom h by A46, FINSEQ_3:27;
then A62: s . 1 = x1 by A45, FINSEQ_1:def 7;
len (g /^ ((k + 1) + 1)) in dom (g /^ ((k + 1) + 1)) by A59, FINSEQ_3:27;
then s . (len s) = (g /^ ((k + 1) + 1)) . (len (g /^ ((k + 1) + 1))) by A49, FINSEQ_1:def 7
.= x2 by A2, A52, JORDAN4:18 ;
hence contradiction by A1, A51, A58, A61, A62, Def8; :: thesis:

end;

suppose A63: (k + 1) + 1 >= len g ; :: thesis:

then A64: (k + 1) + 1 = len g by A32, XXREAL_0:1;
g /^ ((k + 1) + 1) = <*> the carrier of FT by A63, FINSEQ_5:35;
then s = h by FINSEQ_1:47;
hence contradiction by A2, A44, A45, A48, A49, A50, A64; :: thesis:

end;

hence S₂[k + 1] by A40, A41, FINTOPO3:31; :: thesis:

end;

for j being Element of NAT holds S₂[j] from NAT_1:sch 1(A29, A30);
hence ( g . (i + 1) in Finf B0,i & ( i >= 1 implies not g . (i + 1) in Finf B0,(i -' 1) ) ) by A7; :: thesis: