let FT be non empty RelStr ; :: thesis: for g being FinSequence of FT

for A being Subset of FT

for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 & FT is symmetric holds

g is inv_continuous

let g be FinSequence of FT; :: thesis: for A being Subset of FT

for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 & FT is symmetric holds

g is inv_continuous

let A be Subset of FT; :: thesis: for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 & FT is symmetric holds

g is inv_continuous

let x1, x2 be Element of FT; :: thesis: ( g is_minimum_path_in A,x1,x2 & FT is symmetric implies g is inv_continuous )

assume that

A1: g is_minimum_path_in A,x1,x2 and

A2: FT is symmetric ; :: thesis: g is inv_continuous

A3: g . 1 = x1 by A1;

A4: g . (len g) = x2 by A1;

A5: g is continuous by A1;

hence 1 <= len g ; :: according to FINTOPO6:def 9 :: thesis: for i, j being Nat

for y being Element of FT st 1 <= i & i <= len g & 1 <= j & j <= len g & y = g . i & i <> j & g . j in U_FT y & not i = j + 1 holds

j = i + 1

let i2, j2 be Nat; :: thesis: for y being Element of FT st 1 <= i2 & i2 <= len g & 1 <= j2 & j2 <= len g & y = g . i2 & i2 <> j2 & g . j2 in U_FT y & not i2 = j2 + 1 holds

j2 = i2 + 1

let y be Element of FT; :: thesis: ( 1 <= i2 & i2 <= len g & 1 <= j2 & j2 <= len g & y = g . i2 & i2 <> j2 & g . j2 in U_FT y & not i2 = j2 + 1 implies j2 = i2 + 1 )

assume that

A6: 1 <= i2 and

A7: i2 <= len g and

A8: 1 <= j2 and

A9: j2 <= len g and

A10: y = g . i2 and

A11: i2 <> j2 and

A12: g . j2 in U_FT y ; :: thesis: ( i2 = j2 + 1 or j2 = i2 + 1 )

A13: rng g c= A by A1;

for A being Subset of FT

for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 & FT is symmetric holds

g is inv_continuous

let g be FinSequence of FT; :: thesis: for A being Subset of FT

for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 & FT is symmetric holds

g is inv_continuous

let A be Subset of FT; :: thesis: for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 & FT is symmetric holds

g is inv_continuous

let x1, x2 be Element of FT; :: thesis: ( g is_minimum_path_in A,x1,x2 & FT is symmetric implies g is inv_continuous )

assume that

A1: g is_minimum_path_in A,x1,x2 and

A2: FT is symmetric ; :: thesis: g is inv_continuous

A3: g . 1 = x1 by A1;

A4: g . (len g) = x2 by A1;

A5: g is continuous by A1;

hence 1 <= len g ; :: according to FINTOPO6:def 9 :: thesis: for i, j being Nat

for y being Element of FT st 1 <= i & i <= len g & 1 <= j & j <= len g & y = g . i & i <> j & g . j in U_FT y & not i = j + 1 holds

j = i + 1

let i2, j2 be Nat; :: thesis: for y being Element of FT st 1 <= i2 & i2 <= len g & 1 <= j2 & j2 <= len g & y = g . i2 & i2 <> j2 & g . j2 in U_FT y & not i2 = j2 + 1 holds

j2 = i2 + 1

let y be Element of FT; :: thesis: ( 1 <= i2 & i2 <= len g & 1 <= j2 & j2 <= len g & y = g . i2 & i2 <> j2 & g . j2 in U_FT y & not i2 = j2 + 1 implies j2 = i2 + 1 )

assume that

A6: 1 <= i2 and

A7: i2 <= len g and

A8: 1 <= j2 and

A9: j2 <= len g and

A10: y = g . i2 and

A11: i2 <> j2 and

A12: g . j2 in U_FT y ; :: thesis: ( i2 = j2 + 1 or j2 = i2 + 1 )

A13: rng g c= A by A1;

hereby :: thesis: verum

assume that

A14: i2 <> j2 + 1 and

A15: j2 <> i2 + 1 ; :: thesis: contradiction

end;A14: i2 <> j2 + 1 and

A15: j2 <> i2 + 1 ; :: thesis: contradiction

per cases
( i2 < j2 or j2 < i2 )
by A11, XXREAL_0:1;

end;

suppose A16:
i2 < j2
; :: thesis: contradiction

set n1 = j2 -' 1;

set n2 = i2;

reconsider n1 = j2 -' 1, n2 = i2 as Element of NAT by ORDINAL1:def 12;

i2 + 1 <= j2 by A16, NAT_1:13;

then i2 + 1 < j2 by A15, XXREAL_0:1;

then i2 < j2 - 1 by XREAL_1:20;

then A17: n1 > n2 by A8, XREAL_1:233;

1 < j2 by A6, A16, XXREAL_0:2;

then 1 + 1 <= j2 by NAT_1:13;

then 1 <= j2 - 1 by XREAL_1:19;

then A18: 1 <= n1 by A8, XREAL_1:233;

set k = (len g) -' n1;

reconsider g2 = (g | n2) ^ (g /^ n1) as FinSequence of FT ;

A19: len (g | n2) = n2 by A7, FINSEQ_1:59;

A20: j2 -' 1 <= j2 by NAT_D:35;

then A21: n1 <= len g by A9, XXREAL_0:2;

then A22: len (g /^ n1) = (len g) - n1 by RFINSEQ:def 1;

A23: (len g) - n1 >= 0 by A21, XREAL_1:48;

then A24: (len g) -' n1 = (len g) - n1 by XREAL_0:def 2;

A25: len g2 = (len (g | n2)) + (len (g /^ n1)) by FINSEQ_1:22

.= n2 + ((len g) - n1) by A21, A19, RFINSEQ:def 1 ;

A26: g2 . 1 = (g | n2) . 1 by A6, A19, FINSEQ_1:64

.= x1 by A3, A6, FINSEQ_3:112 ;

end;set n2 = i2;

reconsider n1 = j2 -' 1, n2 = i2 as Element of NAT by ORDINAL1:def 12;

i2 + 1 <= j2 by A16, NAT_1:13;

then i2 + 1 < j2 by A15, XXREAL_0:1;

then i2 < j2 - 1 by XREAL_1:20;

then A17: n1 > n2 by A8, XREAL_1:233;

1 < j2 by A6, A16, XXREAL_0:2;

then 1 + 1 <= j2 by NAT_1:13;

then 1 <= j2 - 1 by XREAL_1:19;

then A18: 1 <= n1 by A8, XREAL_1:233;

set k = (len g) -' n1;

reconsider g2 = (g | n2) ^ (g /^ n1) as FinSequence of FT ;

A19: len (g | n2) = n2 by A7, FINSEQ_1:59;

A20: j2 -' 1 <= j2 by NAT_D:35;

then A21: n1 <= len g by A9, XXREAL_0:2;

then A22: len (g /^ n1) = (len g) - n1 by RFINSEQ:def 1;

A23: (len g) - n1 >= 0 by A21, XREAL_1:48;

then A24: (len g) -' n1 = (len g) - n1 by XREAL_0:def 2;

A25: len g2 = (len (g | n2)) + (len (g /^ n1)) by FINSEQ_1:22

.= n2 + ((len g) - n1) by A21, A19, RFINSEQ:def 1 ;

A26: g2 . 1 = (g | n2) . 1 by A6, A19, FINSEQ_1:64

.= x1 by A3, A6, FINSEQ_3:112 ;

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( n1 < len g or n1 = len g )
by A21, XXREAL_0:1;

end;

suppose
n1 < len g
; :: thesis: contradiction

then
n1 + 1 <= len g
by NAT_1:13;

then A27: (n1 + 1) - n1 <= (len g) - n1 by XREAL_1:13;

then A28: 0 + 1 <= n2 + ((len g) - n1) by XREAL_1:7;

A29: g2 is continuous

( rng g2 = (rng (g | n2)) \/ (rng (g /^ n1)) & rng (g | n2) c= rng g ) by FINSEQ_1:31, FINSEQ_5:19;

then rng g2 c= rng g by A51, XBOOLE_1:8;

then A52: rng g2 c= A by A13;

A53: ((len g) -' n1) + n1 = len g by A24;

A54: (len g) -' n1 in dom (g /^ n1) by A24, A22, A27, FINSEQ_3:25;

then g2 . ((len (g | n2)) + ((len g) -' n1)) = (g /^ n1) . ((len g) -' n1) by FINSEQ_1:def 7

.= x2 by A4, A21, A54, A53, RFINSEQ:def 1 ;

then g2 . (len g2) = x2 by A19, A25, A23, XREAL_0:def 2;

then len g <= len g2 by A1, A26, A52, A29;

then (len g) - n2 <= (n2 + ((len g) - n1)) - n2 by A25, XREAL_1:13;

hence contradiction by A17, XREAL_1:10; :: thesis: verum

end;then A27: (n1 + 1) - n1 <= (len g) - n1 by XREAL_1:13;

then A28: 0 + 1 <= n2 + ((len g) - n1) by XREAL_1:7;

A29: g2 is continuous

proof

A51:
rng (g /^ n1) c= rng g
by FINSEQ_5:33;
thus
len g2 >= 1
by A25, A28; :: according to FINTOPO6:def 6 :: thesis: for i being Nat

for x1 being Element of FT st 1 <= i & i < len g2 & x1 = g2 . i holds

g2 . (i + 1) in U_FT x1

let i be Nat; :: thesis: for x1 being Element of FT st 1 <= i & i < len g2 & x1 = g2 . i holds

g2 . (i + 1) in U_FT x1

let z1 be Element of FT; :: thesis: ( 1 <= i & i < len g2 & z1 = g2 . i implies g2 . (i + 1) in U_FT z1 )

assume that

A30: 1 <= i and

A31: i < len g2 and

A32: z1 = g2 . i ; :: thesis: g2 . (i + 1) in U_FT z1

A33: i + 1 <= len g2 by A31, NAT_1:13;

reconsider i = i as Element of NAT by ORDINAL1:def 12;

1 < i + 1 by A30, NAT_1:13;

then i + 1 in dom g2 by A33, FINSEQ_3:25;

then g2 . (i + 1) = g2 /. (i + 1) by PARTFUN1:def 6;

then reconsider z2 = g2 . (i + 1) as Element of FT ;

end;for x1 being Element of FT st 1 <= i & i < len g2 & x1 = g2 . i holds

g2 . (i + 1) in U_FT x1

let i be Nat; :: thesis: for x1 being Element of FT st 1 <= i & i < len g2 & x1 = g2 . i holds

g2 . (i + 1) in U_FT x1

let z1 be Element of FT; :: thesis: ( 1 <= i & i < len g2 & z1 = g2 . i implies g2 . (i + 1) in U_FT z1 )

assume that

A30: 1 <= i and

A31: i < len g2 and

A32: z1 = g2 . i ; :: thesis: g2 . (i + 1) in U_FT z1

A33: i + 1 <= len g2 by A31, NAT_1:13;

reconsider i = i as Element of NAT by ORDINAL1:def 12;

1 < i + 1 by A30, NAT_1:13;

then i + 1 in dom g2 by A33, FINSEQ_3:25;

then g2 . (i + 1) = g2 /. (i + 1) by PARTFUN1:def 6;

then reconsider z2 = g2 . (i + 1) as Element of FT ;

per cases
( i < n2 or i >= n2 )
;

end;

suppose A34:
i < n2
; :: thesis: g2 . (i + 1) in U_FT z1

then A35:
i + 1 <= n2
by NAT_1:13;

i + 1 <= len (g | n2) by A19, A34, NAT_1:13;

then A36: z2 = (g | n2) . (i + 1) by FINSEQ_1:64, NAT_1:12

.= g . (i + 1) by A35, FINSEQ_3:112 ;

A37: i < len g by A7, A34, XXREAL_0:2;

z1 = (g | n2) . i by A19, A30, A32, A34, FINSEQ_1:64

.= g . i by A34, FINSEQ_3:112 ;

hence g2 . (i + 1) in U_FT z1 by A5, A30, A37, A36; :: thesis: verum

end;i + 1 <= len (g | n2) by A19, A34, NAT_1:13;

then A36: z2 = (g | n2) . (i + 1) by FINSEQ_1:64, NAT_1:12

.= g . (i + 1) by A35, FINSEQ_3:112 ;

A37: i < len g by A7, A34, XXREAL_0:2;

z1 = (g | n2) . i by A19, A30, A32, A34, FINSEQ_1:64

.= g . i by A34, FINSEQ_3:112 ;

hence g2 . (i + 1) in U_FT z1 by A5, A30, A37, A36; :: thesis: verum

suppose A38:
i >= n2
; :: thesis: g2 . (i + 1) in U_FT z1

i - n2 < (n2 + ((len g) - n1)) - n2
by A25, A31, XREAL_1:9;

then A39: i -' n2 < (len g) - n1 by A38, XREAL_1:233;

then i -' n2 < (len g) -' n1 by A9, A20, XREAL_1:233, XXREAL_0:2;

then (i -' n2) + 1 <= (len g) -' n1 by NAT_1:13;

then A40: (i -' n2) + 1 <= len (g /^ n1) by A9, A20, A22, XREAL_1:233, XXREAL_0:2;

A41: (len (g | n2)) + (i -' n2) = n2 + (i - n2) by A19, A38, XREAL_1:233

.= i ;

A42: (len (g | n2)) + ((i -' n2) + 1) = ((i - n2) + 1) + n2 by A19, A38, XREAL_1:233

.= i + 1 ;

1 <= (i -' n2) + 1 by NAT_1:12;

then A43: (i -' n2) + 1 in dom (g /^ n1) by A40, FINSEQ_3:25;

end;then A39: i -' n2 < (len g) - n1 by A38, XREAL_1:233;

then i -' n2 < (len g) -' n1 by A9, A20, XREAL_1:233, XXREAL_0:2;

then (i -' n2) + 1 <= (len g) -' n1 by NAT_1:13;

then A40: (i -' n2) + 1 <= len (g /^ n1) by A9, A20, A22, XREAL_1:233, XXREAL_0:2;

A41: (len (g | n2)) + (i -' n2) = n2 + (i - n2) by A19, A38, XREAL_1:233

.= i ;

A42: (len (g | n2)) + ((i -' n2) + 1) = ((i - n2) + 1) + n2 by A19, A38, XREAL_1:233

.= i + 1 ;

1 <= (i -' n2) + 1 by NAT_1:12;

then A43: (i -' n2) + 1 in dom (g /^ n1) by A40, FINSEQ_3:25;

per cases
( i > n2 or i = n2 )
by A38, XXREAL_0:1;

end;

suppose
i > n2
; :: thesis: g2 . (i + 1) in U_FT z1

then A44:
i - n2 > 0
by XREAL_1:50;

then i -' n2 = i - n2 by XREAL_0:def 2;

then A45: 0 + 1 <= i -' n2 by A44, NAT_1:13;

then A46: i -' n2 in dom (g /^ n1) by A22, A39, FINSEQ_3:25;

A47: z2 = (g /^ n1) . ((i -' n2) + 1) by A40, A42, FINSEQ_1:65, NAT_1:12

.= g . (((i -' n2) + 1) + n1) by A21, A43, RFINSEQ:def 1

.= g . (((i -' n2) + n1) + 1) ;

A48: ( 1 <= (i -' n2) + n1 & (i -' n2) + n1 < ((len g) - n1) + n1 ) by A18, A39, NAT_1:12, XREAL_1:6;

z1 = (g /^ n1) . (i -' n2) by A22, A32, A39, A41, A45, FINSEQ_1:65

.= g . ((i -' n2) + n1) by A21, A46, RFINSEQ:def 1 ;

hence g2 . (i + 1) in U_FT z1 by A5, A47, A48; :: thesis: verum

end;then i -' n2 = i - n2 by XREAL_0:def 2;

then A45: 0 + 1 <= i -' n2 by A44, NAT_1:13;

then A46: i -' n2 in dom (g /^ n1) by A22, A39, FINSEQ_3:25;

A47: z2 = (g /^ n1) . ((i -' n2) + 1) by A40, A42, FINSEQ_1:65, NAT_1:12

.= g . (((i -' n2) + 1) + n1) by A21, A43, RFINSEQ:def 1

.= g . (((i -' n2) + n1) + 1) ;

A48: ( 1 <= (i -' n2) + n1 & (i -' n2) + n1 < ((len g) - n1) + n1 ) by A18, A39, NAT_1:12, XREAL_1:6;

z1 = (g /^ n1) . (i -' n2) by A22, A32, A39, A41, A45, FINSEQ_1:65

.= g . ((i -' n2) + n1) by A21, A46, RFINSEQ:def 1 ;

hence g2 . (i + 1) in U_FT z1 by A5, A47, A48; :: thesis: verum

suppose A49:
i = n2
; :: thesis: g2 . (i + 1) in U_FT z1

then A50: z1 =
(g | n2) . n2
by A19, A30, A32, FINSEQ_1:64

.= y by A10, FINSEQ_3:112 ;

z2 = (g /^ n1) . ((i -' n2) + 1) by A40, A42, FINSEQ_1:65, NAT_1:12

.= g . (((i -' n2) + 1) + n1) by A21, A43, RFINSEQ:def 1

.= g . (((i -' n2) + n1) + 1)

.= g . ((0 + (j2 -' 1)) + 1) by A49, XREAL_1:232

.= g . ((j2 - 1) + 1) by A8, XREAL_1:233 ;

hence g2 . (i + 1) in U_FT z1 by A12, A50; :: thesis: verum

end;.= y by A10, FINSEQ_3:112 ;

z2 = (g /^ n1) . ((i -' n2) + 1) by A40, A42, FINSEQ_1:65, NAT_1:12

.= g . (((i -' n2) + 1) + n1) by A21, A43, RFINSEQ:def 1

.= g . (((i -' n2) + n1) + 1)

.= g . ((0 + (j2 -' 1)) + 1) by A49, XREAL_1:232

.= g . ((j2 - 1) + 1) by A8, XREAL_1:233 ;

hence g2 . (i + 1) in U_FT z1 by A12, A50; :: thesis: verum

( rng g2 = (rng (g | n2)) \/ (rng (g /^ n1)) & rng (g | n2) c= rng g ) by FINSEQ_1:31, FINSEQ_5:19;

then rng g2 c= rng g by A51, XBOOLE_1:8;

then A52: rng g2 c= A by A13;

A53: ((len g) -' n1) + n1 = len g by A24;

A54: (len g) -' n1 in dom (g /^ n1) by A24, A22, A27, FINSEQ_3:25;

then g2 . ((len (g | n2)) + ((len g) -' n1)) = (g /^ n1) . ((len g) -' n1) by FINSEQ_1:def 7

.= x2 by A4, A21, A54, A53, RFINSEQ:def 1 ;

then g2 . (len g2) = x2 by A19, A25, A23, XREAL_0:def 2;

then len g <= len g2 by A1, A26, A52, A29;

then (len g) - n2 <= (n2 + ((len g) - n1)) - n2 by A25, XREAL_1:13;

hence contradiction by A17, XREAL_1:10; :: thesis: verum

suppose
n1 = len g
; :: thesis: contradiction

then
j2 - 1 = len g
by A8, XREAL_1:233;

then j2 = (len g) + 1 ;

hence contradiction by A9, NAT_1:13; :: thesis: verum

end;then j2 = (len g) + 1 ;

hence contradiction by A9, NAT_1:13; :: thesis: verum

suppose A55:
j2 < i2
; :: thesis: contradiction

reconsider n1 = i2 -' 1, n2 = j2 as Element of NAT by ORDINAL1:def 12;

j2 + 1 <= i2 by A55, NAT_1:13;

then j2 + 1 < i2 by A14, XXREAL_0:1;

then j2 < i2 - 1 by XREAL_1:20;

then A56: n1 > n2 by A6, XREAL_1:233;

1 < i2 by A8, A55, XXREAL_0:2;

then 1 + 1 <= i2 by NAT_1:13;

then 1 <= i2 - 1 by XREAL_1:19;

then A57: 1 <= n1 by A6, XREAL_1:233;

set k = (len g) -' n1;

reconsider g2 = (g | n2) ^ (g /^ n1) as FinSequence of FT ;

A58: len (g | n2) = n2 by A9, FINSEQ_1:59;

A59: i2 -' 1 <= i2 by NAT_D:35;

then A60: n1 <= len g by A7, XXREAL_0:2;

then A61: len (g /^ n1) = (len g) - n1 by RFINSEQ:def 1;

A62: (len g) - n1 >= 0 by A60, XREAL_1:48;

then A63: (len g) -' n1 = (len g) - n1 by XREAL_0:def 2;

A64: len g2 = (len (g | n2)) + (len (g /^ n1)) by FINSEQ_1:22

.= n2 + ((len g) - n1) by A60, A58, RFINSEQ:def 1 ;

A65: g2 . 1 = (g | n2) . 1 by A8, A58, FINSEQ_1:64

.= x1 by A3, A8, FINSEQ_3:112 ;

end;j2 + 1 <= i2 by A55, NAT_1:13;

then j2 + 1 < i2 by A14, XXREAL_0:1;

then j2 < i2 - 1 by XREAL_1:20;

then A56: n1 > n2 by A6, XREAL_1:233;

1 < i2 by A8, A55, XXREAL_0:2;

then 1 + 1 <= i2 by NAT_1:13;

then 1 <= i2 - 1 by XREAL_1:19;

then A57: 1 <= n1 by A6, XREAL_1:233;

set k = (len g) -' n1;

reconsider g2 = (g | n2) ^ (g /^ n1) as FinSequence of FT ;

A58: len (g | n2) = n2 by A9, FINSEQ_1:59;

A59: i2 -' 1 <= i2 by NAT_D:35;

then A60: n1 <= len g by A7, XXREAL_0:2;

then A61: len (g /^ n1) = (len g) - n1 by RFINSEQ:def 1;

A62: (len g) - n1 >= 0 by A60, XREAL_1:48;

then A63: (len g) -' n1 = (len g) - n1 by XREAL_0:def 2;

A64: len g2 = (len (g | n2)) + (len (g /^ n1)) by FINSEQ_1:22

.= n2 + ((len g) - n1) by A60, A58, RFINSEQ:def 1 ;

A65: g2 . 1 = (g | n2) . 1 by A8, A58, FINSEQ_1:64

.= x1 by A3, A8, FINSEQ_3:112 ;

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( n1 < len g or n1 = len g )
by A60, XXREAL_0:1;

end;

suppose
n1 < len g
; :: thesis: contradiction

then
n1 + 1 <= len g
by NAT_1:13;

then A66: (n1 + 1) - n1 <= (len g) - n1 by XREAL_1:13;

then A67: 0 + 1 <= n2 + ((len g) - n1) by XREAL_1:7;

A68: g2 is continuous

( rng g2 = (rng (g | n2)) \/ (rng (g /^ n1)) & rng (g | n2) c= rng g ) by FINSEQ_1:31, FINSEQ_5:19;

then rng g2 c= rng g by A90, XBOOLE_1:8;

then A91: rng g2 c= A by A13;

A92: ((len g) -' n1) + n1 = len g by A63;

A93: (len g) -' n1 in dom (g /^ n1) by A63, A61, A66, FINSEQ_3:25;

then g2 . ((len (g | n2)) + ((len g) -' n1)) = (g /^ n1) . ((len g) -' n1) by FINSEQ_1:def 7

.= x2 by A4, A60, A93, A92, RFINSEQ:def 1 ;

then g2 . (len g2) = x2 by A58, A64, A62, XREAL_0:def 2;

then len g <= len g2 by A1, A65, A91, A68;

then (len g) - n2 <= (n2 + ((len g) - n1)) - n2 by A64, XREAL_1:13;

hence contradiction by A56, XREAL_1:10; :: thesis: verum

end;then A66: (n1 + 1) - n1 <= (len g) - n1 by XREAL_1:13;

then A67: 0 + 1 <= n2 + ((len g) - n1) by XREAL_1:7;

A68: g2 is continuous

proof

A90:
rng (g /^ n1) c= rng g
by FINSEQ_5:33;
thus
len g2 >= 1
by A64, A67; :: according to FINTOPO6:def 6 :: thesis: for i being Nat

for x1 being Element of FT st 1 <= i & i < len g2 & x1 = g2 . i holds

g2 . (i + 1) in U_FT x1

let i be Nat; :: thesis: for x1 being Element of FT st 1 <= i & i < len g2 & x1 = g2 . i holds

g2 . (i + 1) in U_FT x1

let z1 be Element of FT; :: thesis: ( 1 <= i & i < len g2 & z1 = g2 . i implies g2 . (i + 1) in U_FT z1 )

assume that

A69: 1 <= i and

A70: i < len g2 and

A71: z1 = g2 . i ; :: thesis: g2 . (i + 1) in U_FT z1

A72: i + 1 <= len g2 by A70, NAT_1:13;

reconsider i = i as Element of NAT by ORDINAL1:def 12;

1 < i + 1 by A69, NAT_1:13;

then i + 1 in dom g2 by A72, FINSEQ_3:25;

then g2 . (i + 1) = g2 /. (i + 1) by PARTFUN1:def 6;

then reconsider z2 = g2 . (i + 1) as Element of FT ;

end;for x1 being Element of FT st 1 <= i & i < len g2 & x1 = g2 . i holds

g2 . (i + 1) in U_FT x1

let i be Nat; :: thesis: for x1 being Element of FT st 1 <= i & i < len g2 & x1 = g2 . i holds

g2 . (i + 1) in U_FT x1

let z1 be Element of FT; :: thesis: ( 1 <= i & i < len g2 & z1 = g2 . i implies g2 . (i + 1) in U_FT z1 )

assume that

A69: 1 <= i and

A70: i < len g2 and

A71: z1 = g2 . i ; :: thesis: g2 . (i + 1) in U_FT z1

A72: i + 1 <= len g2 by A70, NAT_1:13;

reconsider i = i as Element of NAT by ORDINAL1:def 12;

1 < i + 1 by A69, NAT_1:13;

then i + 1 in dom g2 by A72, FINSEQ_3:25;

then g2 . (i + 1) = g2 /. (i + 1) by PARTFUN1:def 6;

then reconsider z2 = g2 . (i + 1) as Element of FT ;

per cases
( i < n2 or i >= n2 )
;

end;

suppose A73:
i < n2
; :: thesis: g2 . (i + 1) in U_FT z1

then A74:
i + 1 <= n2
by NAT_1:13;

i + 1 <= len (g | n2) by A58, A73, NAT_1:13;

then A75: z2 = (g | n2) . (i + 1) by FINSEQ_1:64, NAT_1:12

.= g . (i + 1) by A74, FINSEQ_3:112 ;

A76: i < len g by A9, A73, XXREAL_0:2;

z1 = (g | n2) . i by A58, A69, A71, A73, FINSEQ_1:64

.= g . i by A73, FINSEQ_3:112 ;

hence g2 . (i + 1) in U_FT z1 by A5, A69, A76, A75; :: thesis: verum

end;i + 1 <= len (g | n2) by A58, A73, NAT_1:13;

then A75: z2 = (g | n2) . (i + 1) by FINSEQ_1:64, NAT_1:12

.= g . (i + 1) by A74, FINSEQ_3:112 ;

A76: i < len g by A9, A73, XXREAL_0:2;

z1 = (g | n2) . i by A58, A69, A71, A73, FINSEQ_1:64

.= g . i by A73, FINSEQ_3:112 ;

hence g2 . (i + 1) in U_FT z1 by A5, A69, A76, A75; :: thesis: verum

suppose A77:
i >= n2
; :: thesis: g2 . (i + 1) in U_FT z1

i - n2 < (n2 + ((len g) - n1)) - n2
by A64, A70, XREAL_1:9;

then A78: i -' n2 < (len g) - n1 by A77, XREAL_1:233;

then i -' n2 < (len g) -' n1 by A7, A59, XREAL_1:233, XXREAL_0:2;

then (i -' n2) + 1 <= (len g) -' n1 by NAT_1:13;

then A79: (i -' n2) + 1 <= len (g /^ n1) by A7, A59, A61, XREAL_1:233, XXREAL_0:2;

A80: (len (g | n2)) + (i -' n2) = n2 + (i - n2) by A58, A77, XREAL_1:233

.= i ;

A81: (len (g | n2)) + ((i -' n2) + 1) = ((i - n2) + 1) + n2 by A58, A77, XREAL_1:233

.= i + 1 ;

1 <= (i -' n2) + 1 by NAT_1:12;

then A82: (i -' n2) + 1 in dom (g /^ n1) by A79, FINSEQ_3:25;

end;then A78: i -' n2 < (len g) - n1 by A77, XREAL_1:233;

then i -' n2 < (len g) -' n1 by A7, A59, XREAL_1:233, XXREAL_0:2;

then (i -' n2) + 1 <= (len g) -' n1 by NAT_1:13;

then A79: (i -' n2) + 1 <= len (g /^ n1) by A7, A59, A61, XREAL_1:233, XXREAL_0:2;

A80: (len (g | n2)) + (i -' n2) = n2 + (i - n2) by A58, A77, XREAL_1:233

.= i ;

A81: (len (g | n2)) + ((i -' n2) + 1) = ((i - n2) + 1) + n2 by A58, A77, XREAL_1:233

.= i + 1 ;

1 <= (i -' n2) + 1 by NAT_1:12;

then A82: (i -' n2) + 1 in dom (g /^ n1) by A79, FINSEQ_3:25;

per cases
( i > n2 or i = n2 )
by A77, XXREAL_0:1;

end;

suppose
i > n2
; :: thesis: g2 . (i + 1) in U_FT z1

then A83:
i - n2 > 0
by XREAL_1:50;

then i -' n2 = i - n2 by XREAL_0:def 2;

then A84: 0 + 1 <= i -' n2 by A83, NAT_1:13;

then A85: i -' n2 in dom (g /^ n1) by A61, A78, FINSEQ_3:25;

A86: z2 = (g /^ n1) . ((i -' n2) + 1) by A79, A81, FINSEQ_1:65, NAT_1:12

.= g . (((i -' n2) + 1) + n1) by A60, A82, RFINSEQ:def 1

.= g . (((i -' n2) + n1) + 1) ;

A87: ( 1 <= (i -' n2) + n1 & (i -' n2) + n1 < ((len g) - n1) + n1 ) by A57, A78, NAT_1:12, XREAL_1:6;

z1 = (g /^ n1) . (i -' n2) by A61, A71, A78, A80, A84, FINSEQ_1:65

.= g . ((i -' n2) + n1) by A60, A85, RFINSEQ:def 1 ;

hence g2 . (i + 1) in U_FT z1 by A5, A86, A87; :: thesis: verum

end;then i -' n2 = i - n2 by XREAL_0:def 2;

then A84: 0 + 1 <= i -' n2 by A83, NAT_1:13;

then A85: i -' n2 in dom (g /^ n1) by A61, A78, FINSEQ_3:25;

A86: z2 = (g /^ n1) . ((i -' n2) + 1) by A79, A81, FINSEQ_1:65, NAT_1:12

.= g . (((i -' n2) + 1) + n1) by A60, A82, RFINSEQ:def 1

.= g . (((i -' n2) + n1) + 1) ;

A87: ( 1 <= (i -' n2) + n1 & (i -' n2) + n1 < ((len g) - n1) + n1 ) by A57, A78, NAT_1:12, XREAL_1:6;

z1 = (g /^ n1) . (i -' n2) by A61, A71, A78, A80, A84, FINSEQ_1:65

.= g . ((i -' n2) + n1) by A60, A85, RFINSEQ:def 1 ;

hence g2 . (i + 1) in U_FT z1 by A5, A86, A87; :: thesis: verum

suppose A88:
i = n2
; :: thesis: g2 . (i + 1) in U_FT z1

then A89: z1 =
(g | n2) . n2
by A58, A69, A71, FINSEQ_1:64

.= g . j2 by FINSEQ_3:112 ;

z2 = (g /^ n1) . ((i -' n2) + 1) by A79, A81, FINSEQ_1:65, NAT_1:12

.= g . (((i -' n2) + 1) + n1) by A60, A82, RFINSEQ:def 1

.= g . (((i -' n2) + n1) + 1)

.= g . ((0 + (i2 -' 1)) + 1) by A88, XREAL_1:232

.= g . ((i2 - 1) + 1) by A6, XREAL_1:233

.= y by A10 ;

hence g2 . (i + 1) in U_FT z1 by A2, A12, A89; :: thesis: verum

end;.= g . j2 by FINSEQ_3:112 ;

z2 = (g /^ n1) . ((i -' n2) + 1) by A79, A81, FINSEQ_1:65, NAT_1:12

.= g . (((i -' n2) + 1) + n1) by A60, A82, RFINSEQ:def 1

.= g . (((i -' n2) + n1) + 1)

.= g . ((0 + (i2 -' 1)) + 1) by A88, XREAL_1:232

.= g . ((i2 - 1) + 1) by A6, XREAL_1:233

.= y by A10 ;

hence g2 . (i + 1) in U_FT z1 by A2, A12, A89; :: thesis: verum

( rng g2 = (rng (g | n2)) \/ (rng (g /^ n1)) & rng (g | n2) c= rng g ) by FINSEQ_1:31, FINSEQ_5:19;

then rng g2 c= rng g by A90, XBOOLE_1:8;

then A91: rng g2 c= A by A13;

A92: ((len g) -' n1) + n1 = len g by A63;

A93: (len g) -' n1 in dom (g /^ n1) by A63, A61, A66, FINSEQ_3:25;

then g2 . ((len (g | n2)) + ((len g) -' n1)) = (g /^ n1) . ((len g) -' n1) by FINSEQ_1:def 7

.= x2 by A4, A60, A93, A92, RFINSEQ:def 1 ;

then g2 . (len g2) = x2 by A58, A64, A62, XREAL_0:def 2;

then len g <= len g2 by A1, A65, A91, A68;

then (len g) - n2 <= (n2 + ((len g) - n1)) - n2 by A64, XREAL_1:13;

hence contradiction by A56, XREAL_1:10; :: thesis: verum

suppose
n1 = len g
; :: thesis: contradiction

then
i2 - 1 = len g
by A6, XREAL_1:233;

then i2 = (len g) + 1 ;

hence contradiction by A7, NAT_1:13; :: thesis: verum

end;then i2 = (len g) + 1 ;

hence contradiction by A7, NAT_1:13; :: thesis: verum