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 holds

g is one-to-one

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 holds

g is one-to-one

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

g is one-to-one

let x1, x2 be Element of FT; :: thesis: ( g is_minimum_path_in A,x1,x2 implies g is one-to-one )

assume A1: g is_minimum_path_in A,x1,x2 ; :: thesis: g is one-to-one

then A2: g is continuous ;

A3: 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 A1;

A4: rng g c= A by A1;

A5: g . 1 = x1 by A1;

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

assume not g is one-to-one ; :: thesis: contradiction

then consider y1, y2 being object such that

A7: y1 in dom g and

A8: y2 in dom g and

A9: g . y1 = g . y2 and

A10: y1 <> y2 by FUNCT_1:def 4;

reconsider n1 = y1, n2 = y2 as Element of NAT by A7, A8;

A11: dom g = Seg (len g) by FINSEQ_1:def 3;

then A12: 1 <= n1 by A7, FINSEQ_1:1;

A13: n2 <= len g by A8, A11, FINSEQ_1:1;

A14: 1 <= n2 by A8, A11, FINSEQ_1:1;

A15: n1 <= len g by A7, A11, FINSEQ_1:1;

for A being Subset of FT

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

g is one-to-one

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 holds

g is one-to-one

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

g is one-to-one

let x1, x2 be Element of FT; :: thesis: ( g is_minimum_path_in A,x1,x2 implies g is one-to-one )

assume A1: g is_minimum_path_in A,x1,x2 ; :: thesis: g is one-to-one

then A2: g is continuous ;

A3: 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 A1;

A4: rng g c= A by A1;

A5: g . 1 = x1 by A1;

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

assume not g is one-to-one ; :: thesis: contradiction

then consider y1, y2 being object such that

A7: y1 in dom g and

A8: y2 in dom g and

A9: g . y1 = g . y2 and

A10: y1 <> y2 by FUNCT_1:def 4;

reconsider n1 = y1, n2 = y2 as Element of NAT by A7, A8;

A11: dom g = Seg (len g) by FINSEQ_1:def 3;

then A12: 1 <= n1 by A7, FINSEQ_1:1;

A13: n2 <= len g by A8, A11, FINSEQ_1:1;

A14: 1 <= n2 by A8, A11, FINSEQ_1:1;

A15: n1 <= len g by A7, A11, FINSEQ_1:1;

per cases
( n1 > n2 or n2 > n1 )
by A10, XXREAL_0:1;

end;

suppose A16:
n1 > n2
; :: thesis: contradiction

set k = (len g) -' n1;

set g2 = (g | n2) ^ (g /^ n1);

A17: len (g /^ n1) = (len g) - n1 by A15, RFINSEQ:def 1;

A18: (len g) - n1 >= 0 by A15, XREAL_1:48;

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

A20: len (g | n2) = n2 by A13, FINSEQ_1:59;

then A21: ((g | n2) ^ (g /^ n1)) . 1 = (g | n2) . 1 by A14, FINSEQ_1:64

.= g . 1 by A14, FINSEQ_3:112 ;

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

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

end;set g2 = (g | n2) ^ (g /^ n1);

A17: len (g /^ n1) = (len g) - n1 by A15, RFINSEQ:def 1;

A18: (len g) - n1 >= 0 by A15, XREAL_1:48;

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

A20: len (g | n2) = n2 by A13, FINSEQ_1:59;

then A21: ((g | n2) ^ (g /^ n1)) . 1 = (g | n2) . 1 by A14, FINSEQ_1:64

.= g . 1 by A14, FINSEQ_3:112 ;

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

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

per cases
( n1 < len g or n1 = len g )
by A15, XXREAL_0:1;

end;

suppose
n1 < len g
; :: thesis: contradiction

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

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

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

A25: (g | n2) ^ (g /^ n1) is continuous

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

then A47: rng ((g | n2) ^ (g /^ n1)) c= rng g by A46, XBOOLE_1:8;

A48: ((len g) -' n1) + n1 = len g by A19;

A49: (len g) -' n1 in dom (g /^ n1) by A19, A17, A23, FINSEQ_3:25;

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

.= x2 by A6, A15, A49, A48, RFINSEQ:def 1 ;

then ((g | n2) ^ (g /^ n1)) . (len ((g | n2) ^ (g /^ n1))) = x2 by A20, A22, A18, XREAL_0:def 2;

then len g <= len ((g | n2) ^ (g /^ n1)) by A4, A5, A3, A21, A47, A25, XBOOLE_1:1;

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

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

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

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

A25: (g | n2) ^ (g /^ n1) is continuous

proof

A46:
rng (g /^ n1) c= rng g
by FINSEQ_5:33;
thus
len ((g | n2) ^ (g /^ n1)) >= 1
by A22, A24; :: according to FINTOPO6:def 6 :: thesis: for i being Nat

for x1 being Element of FT st 1 <= i & i < len ((g | n2) ^ (g /^ n1)) & x1 = ((g | n2) ^ (g /^ n1)) . i holds

((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT x1

let i be Nat; :: thesis: for x1 being Element of FT st 1 <= i & i < len ((g | n2) ^ (g /^ n1)) & x1 = ((g | n2) ^ (g /^ n1)) . i holds

((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT x1

let z1 be Element of FT; :: thesis: ( 1 <= i & i < len ((g | n2) ^ (g /^ n1)) & z1 = ((g | n2) ^ (g /^ n1)) . i implies ((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT z1 )

assume that

A26: 1 <= i and

A27: i < len ((g | n2) ^ (g /^ n1)) and

A28: z1 = ((g | n2) ^ (g /^ n1)) . i ; :: thesis: ((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT z1

A29: i + 1 <= len ((g | n2) ^ (g /^ n1)) by A27, NAT_1:13;

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

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

then i + 1 in dom ((g | n2) ^ (g /^ n1)) by A29, FINSEQ_3:25;

then ((g | n2) ^ (g /^ n1)) . (i + 1) = ((g | n2) ^ (g /^ n1)) /. (i + 1) by PARTFUN1:def 6;

then reconsider z2 = ((g | n2) ^ (g /^ n1)) . (i + 1) as Element of FT ;

end;for x1 being Element of FT st 1 <= i & i < len ((g | n2) ^ (g /^ n1)) & x1 = ((g | n2) ^ (g /^ n1)) . i holds

((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT x1

let i be Nat; :: thesis: for x1 being Element of FT st 1 <= i & i < len ((g | n2) ^ (g /^ n1)) & x1 = ((g | n2) ^ (g /^ n1)) . i holds

((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT x1

let z1 be Element of FT; :: thesis: ( 1 <= i & i < len ((g | n2) ^ (g /^ n1)) & z1 = ((g | n2) ^ (g /^ n1)) . i implies ((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT z1 )

assume that

A26: 1 <= i and

A27: i < len ((g | n2) ^ (g /^ n1)) and

A28: z1 = ((g | n2) ^ (g /^ n1)) . i ; :: thesis: ((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT z1

A29: i + 1 <= len ((g | n2) ^ (g /^ n1)) by A27, NAT_1:13;

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

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

then i + 1 in dom ((g | n2) ^ (g /^ n1)) by A29, FINSEQ_3:25;

then ((g | n2) ^ (g /^ n1)) . (i + 1) = ((g | n2) ^ (g /^ n1)) /. (i + 1) by PARTFUN1:def 6;

then reconsider z2 = ((g | n2) ^ (g /^ n1)) . (i + 1) as Element of FT ;

now :: thesis: z2 in U_FT z1end;

hence
((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT z1
; :: thesis: verumper cases
( i < n2 or i >= n2 )
;

end;

suppose A30:
i < n2
; :: thesis: z2 in U_FT z1

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

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

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

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

A33: i < len g by A13, A30, XXREAL_0:2;

z1 = (g | n2) . i by A20, A26, A28, A30, FINSEQ_1:64

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

hence z2 in U_FT z1 by A2, A26, A33, A32; :: thesis: verum

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

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

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

A33: i < len g by A13, A30, XXREAL_0:2;

z1 = (g | n2) . i by A20, A26, A28, A30, FINSEQ_1:64

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

hence z2 in U_FT z1 by A2, A26, A33, A32; :: thesis: verum

suppose A34:
i >= n2
; :: thesis: z2 in U_FT z1

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

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

then A36: (i -' n2) + n1 < ((len g) - n1) + n1 by XREAL_1:6;

A37: (len (g | n2)) + (i -' n2) = n2 + (i - n2) by A20, A34, XREAL_1:233

.= i ;

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

then A43: (i -' n2) + 1 <= len (g /^ n1) by A15, A17, XREAL_1:233;

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

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

(len (g | n2)) + ((i -' n2) + 1) = ((i - n2) + 1) + n2 by A20, A34, XREAL_1:233

.= i + 1 ;

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

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

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

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

hence z2 in U_FT z1 by A2, A38, A45, A36; :: thesis: verum

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

then A36: (i -' n2) + n1 < ((len g) - n1) + n1 by XREAL_1:6;

A37: (len (g | n2)) + (i -' n2) = n2 + (i - n2) by A20, A34, XREAL_1:233

.= i ;

A38: now :: thesis: z1 = g . ((i -' n2) + n1)end;

i -' n2 < (len g) -' n1
by A15, A35, XREAL_1:233;per cases
( i > n2 or i = n2 )
by A34, XXREAL_0:1;

end;

suppose
i > n2
; :: thesis: z1 = g . ((i -' n2) + n1)

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

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

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

then A41: i -' n2 in dom (g /^ n1) by A17, A35, FINSEQ_3:25;

thus z1 = (g /^ n1) . (i -' n2) by A17, A28, A35, A37, A40, FINSEQ_1:65

.= g . ((i -' n2) + n1) by A15, A41, RFINSEQ:def 1 ; :: thesis: verum

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

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

then A41: i -' n2 in dom (g /^ n1) by A17, A35, FINSEQ_3:25;

thus z1 = (g /^ n1) . (i -' n2) by A17, A28, A35, A37, A40, FINSEQ_1:65

.= g . ((i -' n2) + n1) by A15, A41, RFINSEQ:def 1 ; :: thesis: verum

suppose A42:
i = n2
; :: thesis: z1 = g . ((i -' n2) + n1)

hence z1 =
(g | n2) . n2
by A20, A26, A28, FINSEQ_1:64

.= g . (0 + n1) by A9, FINSEQ_3:112

.= g . ((i -' n2) + n1) by A42, XREAL_1:232 ;

:: thesis: verum

end;.= g . (0 + n1) by A9, FINSEQ_3:112

.= g . ((i -' n2) + n1) by A42, XREAL_1:232 ;

:: thesis: verum

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

then A43: (i -' n2) + 1 <= len (g /^ n1) by A15, A17, XREAL_1:233;

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

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

(len (g | n2)) + ((i -' n2) + 1) = ((i - n2) + 1) + n2 by A20, A34, XREAL_1:233

.= i + 1 ;

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

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

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

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

hence z2 in U_FT z1 by A2, A38, A45, A36; :: thesis: verum

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

then A47: rng ((g | n2) ^ (g /^ n1)) c= rng g by A46, XBOOLE_1:8;

A48: ((len g) -' n1) + n1 = len g by A19;

A49: (len g) -' n1 in dom (g /^ n1) by A19, A17, A23, FINSEQ_3:25;

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

.= x2 by A6, A15, A49, A48, RFINSEQ:def 1 ;

then ((g | n2) ^ (g /^ n1)) . (len ((g | n2) ^ (g /^ n1))) = x2 by A20, A22, A18, XREAL_0:def 2;

then len g <= len ((g | n2) ^ (g /^ n1)) by A4, A5, A3, A21, A47, A25, XBOOLE_1:1;

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

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

suppose A50:
n1 = len g
; :: thesis: contradiction

A51:
len (g /^ n1) = (len g) - n1
by A15, RFINSEQ:def 1;

A52: (g | n2) ^ (g /^ n1) is continuous

A74: (g | n2) ^ (g /^ n1) = (g | n2) ^ {} by A50, FINSEQ_6:167

.= g | n2 by FINSEQ_1:34 ;

then ((g | n2) ^ (g /^ n1)) . (len ((g | n2) ^ (g /^ n1))) = x2 by A6, A9, A20, A50, FINSEQ_3:112;

then len g <= len ((g | n2) ^ (g /^ n1)) by A4, A5, A3, A21, A74, A73, A52, XBOOLE_1:1;

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

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

end;A52: (g | n2) ^ (g /^ n1) is continuous

proof

A73:
rng (g | n2) c= rng g
by FINSEQ_5:19;
thus
1 <= len ((g | n2) ^ (g /^ n1))
by A8, A11, A22, A50, FINSEQ_1:1; :: according to FINTOPO6:def 6 :: thesis: for i being Nat

for x1 being Element of FT st 1 <= i & i < len ((g | n2) ^ (g /^ n1)) & x1 = ((g | n2) ^ (g /^ n1)) . i holds

((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT x1

let i be Nat; :: thesis: for x1 being Element of FT st 1 <= i & i < len ((g | n2) ^ (g /^ n1)) & x1 = ((g | n2) ^ (g /^ n1)) . i holds

((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT x1

let z1 be Element of FT; :: thesis: ( 1 <= i & i < len ((g | n2) ^ (g /^ n1)) & z1 = ((g | n2) ^ (g /^ n1)) . i implies ((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT z1 )

assume that

A53: 1 <= i and

A54: i < len ((g | n2) ^ (g /^ n1)) and

A55: z1 = ((g | n2) ^ (g /^ n1)) . i ; :: thesis: ((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT z1

A56: i + 1 <= len ((g | n2) ^ (g /^ n1)) by A54, NAT_1:13;

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

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

then i + 1 in dom ((g | n2) ^ (g /^ n1)) by A56, FINSEQ_3:25;

then ((g | n2) ^ (g /^ n1)) . (i + 1) = ((g | n2) ^ (g /^ n1)) /. (i + 1) by PARTFUN1:def 6;

then reconsider z2 = ((g | n2) ^ (g /^ n1)) . (i + 1) as Element of FT ;

end;for x1 being Element of FT st 1 <= i & i < len ((g | n2) ^ (g /^ n1)) & x1 = ((g | n2) ^ (g /^ n1)) . i holds

((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT x1

let i be Nat; :: thesis: for x1 being Element of FT st 1 <= i & i < len ((g | n2) ^ (g /^ n1)) & x1 = ((g | n2) ^ (g /^ n1)) . i holds

((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT x1

let z1 be Element of FT; :: thesis: ( 1 <= i & i < len ((g | n2) ^ (g /^ n1)) & z1 = ((g | n2) ^ (g /^ n1)) . i implies ((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT z1 )

assume that

A53: 1 <= i and

A54: i < len ((g | n2) ^ (g /^ n1)) and

A55: z1 = ((g | n2) ^ (g /^ n1)) . i ; :: thesis: ((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT z1

A56: i + 1 <= len ((g | n2) ^ (g /^ n1)) by A54, NAT_1:13;

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

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

then i + 1 in dom ((g | n2) ^ (g /^ n1)) by A56, FINSEQ_3:25;

then ((g | n2) ^ (g /^ n1)) . (i + 1) = ((g | n2) ^ (g /^ n1)) /. (i + 1) by PARTFUN1:def 6;

then reconsider z2 = ((g | n2) ^ (g /^ n1)) . (i + 1) as Element of FT ;

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

end;

suppose A57:
i < n2
; :: thesis: ((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT z1

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

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

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

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

A60: i < len g by A13, A57, XXREAL_0:2;

z1 = (g | n2) . i by A20, A53, A55, A57, FINSEQ_1:64

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

hence ((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT z1 by A2, A53, A60, A59; :: thesis: verum

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

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

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

A60: i < len g by A13, A57, XXREAL_0:2;

z1 = (g | n2) . i by A20, A53, A55, A57, FINSEQ_1:64

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

hence ((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT z1 by A2, A53, A60, A59; :: thesis: verum

suppose A61:
i >= n2
; :: thesis: ((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT z1

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

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

then A63: (i -' n2) + n1 < ((len g) - n1) + n1 by XREAL_1:6;

A64: (len (g | n2)) + (i -' n2) = n2 + (i - n2) by A20, A61, XREAL_1:233

.= i ;

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

then A70: (i -' n2) + 1 <= len (g /^ n1) by A15, A51, XREAL_1:233;

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

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

(len (g | n2)) + ((i -' n2) + 1) = ((i - n2) + 1) + n2 by A20, A61, XREAL_1:233

.= i + 1 ;

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

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

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

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

hence ((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT z1 by A2, A65, A72, A63; :: thesis: verum

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

then A63: (i -' n2) + n1 < ((len g) - n1) + n1 by XREAL_1:6;

A64: (len (g | n2)) + (i -' n2) = n2 + (i - n2) by A20, A61, XREAL_1:233

.= i ;

A65: now :: thesis: z1 = g . ((i -' n2) + n1)end;

i -' n2 < (len g) -' n1
by A15, A62, XREAL_1:233;per cases
( i > n2 or i = n2 )
by A61, XXREAL_0:1;

end;

suppose
i > n2
; :: thesis: z1 = g . ((i -' n2) + n1)

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

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

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

then A68: i -' n2 in dom (g /^ n1) by A51, A62, FINSEQ_3:25;

thus z1 = (g /^ n1) . (i -' n2) by A51, A55, A62, A64, A67, FINSEQ_1:65

.= g . ((i -' n2) + n1) by A15, A68, RFINSEQ:def 1 ; :: thesis: verum

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

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

then A68: i -' n2 in dom (g /^ n1) by A51, A62, FINSEQ_3:25;

thus z1 = (g /^ n1) . (i -' n2) by A51, A55, A62, A64, A67, FINSEQ_1:65

.= g . ((i -' n2) + n1) by A15, A68, RFINSEQ:def 1 ; :: thesis: verum

suppose A69:
i = n2
; :: thesis: z1 = g . ((i -' n2) + n1)

hence z1 =
(g | n2) . n2
by A20, A53, A55, FINSEQ_1:64

.= g . (0 + n1) by A9, FINSEQ_3:112

.= g . ((i -' n2) + n1) by A69, XREAL_1:232 ;

:: thesis: verum

end;.= g . (0 + n1) by A9, FINSEQ_3:112

.= g . ((i -' n2) + n1) by A69, XREAL_1:232 ;

:: thesis: verum

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

then A70: (i -' n2) + 1 <= len (g /^ n1) by A15, A51, XREAL_1:233;

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

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

(len (g | n2)) + ((i -' n2) + 1) = ((i - n2) + 1) + n2 by A20, A61, XREAL_1:233

.= i + 1 ;

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

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

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

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

hence ((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT z1 by A2, A65, A72, A63; :: thesis: verum

A74: (g | n2) ^ (g /^ n1) = (g | n2) ^ {} by A50, FINSEQ_6:167

.= g | n2 by FINSEQ_1:34 ;

then ((g | n2) ^ (g /^ n1)) . (len ((g | n2) ^ (g /^ n1))) = x2 by A6, A9, A20, A50, FINSEQ_3:112;

then len g <= len ((g | n2) ^ (g /^ n1)) by A4, A5, A3, A21, A74, A73, A52, XBOOLE_1:1;

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

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

suppose A75:
n2 > n1
; :: thesis: contradiction

set k = (len g) -' n2;

set g2 = (g | n1) ^ (g /^ n2);

A76: len (g /^ n2) = (len g) - n2 by A13, RFINSEQ:def 1;

(len g) - n2 >= 0 by A13, XREAL_1:48;

then A77: (len g) -' n2 = (len g) - n2 by XREAL_0:def 2;

A78: len (g | n1) = n1 by A15, FINSEQ_1:59;

then A79: ((g | n1) ^ (g /^ n2)) . 1 = (g | n1) . 1 by A12, FINSEQ_1:64

.= x1 by A5, A12, FINSEQ_3:112 ;

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

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

end;set g2 = (g | n1) ^ (g /^ n2);

A76: len (g /^ n2) = (len g) - n2 by A13, RFINSEQ:def 1;

(len g) - n2 >= 0 by A13, XREAL_1:48;

then A77: (len g) -' n2 = (len g) - n2 by XREAL_0:def 2;

A78: len (g | n1) = n1 by A15, FINSEQ_1:59;

then A79: ((g | n1) ^ (g /^ n2)) . 1 = (g | n1) . 1 by A12, FINSEQ_1:64

.= x1 by A5, A12, FINSEQ_3:112 ;

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

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

per cases
( n2 < len g or n2 = len g )
by A13, XXREAL_0:1;

end;

suppose
n2 < len g
; :: thesis: contradiction

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

then A81: (n2 + 1) - n2 <= (len g) - n2 by XREAL_1:13;

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

A83: (g | n1) ^ (g /^ n2) is continuous

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

then rng ((g | n1) ^ (g /^ n2)) c= rng g by A104, XBOOLE_1:8;

then A105: rng ((g | n1) ^ (g /^ n2)) c= A by A4;

A106: ((len g) -' n2) + n2 = len g by A77;

A107: (len g) -' n2 in dom (g /^ n2) by A77, A76, A81, FINSEQ_3:25;

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

.= x2 by A6, A13, A107, A106, RFINSEQ:def 1 ;

then ((g | n1) ^ (g /^ n2)) . (len ((g | n1) ^ (g /^ n2))) = x2 by A15, A80, A77, FINSEQ_1:59;

then len g <= len ((g | n1) ^ (g /^ n2)) by A1, A79, A105, A83;

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

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

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

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

A83: (g | n1) ^ (g /^ n2) is continuous

proof

A104:
rng (g /^ n2) c= rng g
by FINSEQ_5:33;
thus
len ((g | n1) ^ (g /^ n2)) >= 1
by A80, A82; :: according to FINTOPO6:def 6 :: thesis: for i being Nat

for x1 being Element of FT st 1 <= i & i < len ((g | n1) ^ (g /^ n2)) & x1 = ((g | n1) ^ (g /^ n2)) . i holds

((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT x1

let i be Nat; :: thesis: for x1 being Element of FT st 1 <= i & i < len ((g | n1) ^ (g /^ n2)) & x1 = ((g | n1) ^ (g /^ n2)) . i holds

((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT x1

let z1 be Element of FT; :: thesis: ( 1 <= i & i < len ((g | n1) ^ (g /^ n2)) & z1 = ((g | n1) ^ (g /^ n2)) . i implies ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1 )

assume that

A84: 1 <= i and

A85: i < len ((g | n1) ^ (g /^ n2)) and

A86: z1 = ((g | n1) ^ (g /^ n2)) . i ; :: thesis: ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1

A87: i + 1 <= len ((g | n1) ^ (g /^ n2)) by A85, NAT_1:13;

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

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

then i + 1 in dom ((g | n1) ^ (g /^ n2)) by A87, FINSEQ_3:25;

then ((g | n1) ^ (g /^ n2)) . (i + 1) = ((g | n1) ^ (g /^ n2)) /. (i + 1) by PARTFUN1:def 6;

then reconsider z2 = ((g | n1) ^ (g /^ n2)) . (i + 1) as Element of FT ;

end;for x1 being Element of FT st 1 <= i & i < len ((g | n1) ^ (g /^ n2)) & x1 = ((g | n1) ^ (g /^ n2)) . i holds

((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT x1

let i be Nat; :: thesis: for x1 being Element of FT st 1 <= i & i < len ((g | n1) ^ (g /^ n2)) & x1 = ((g | n1) ^ (g /^ n2)) . i holds

((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT x1

let z1 be Element of FT; :: thesis: ( 1 <= i & i < len ((g | n1) ^ (g /^ n2)) & z1 = ((g | n1) ^ (g /^ n2)) . i implies ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1 )

assume that

A84: 1 <= i and

A85: i < len ((g | n1) ^ (g /^ n2)) and

A86: z1 = ((g | n1) ^ (g /^ n2)) . i ; :: thesis: ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1

A87: i + 1 <= len ((g | n1) ^ (g /^ n2)) by A85, NAT_1:13;

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

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

then i + 1 in dom ((g | n1) ^ (g /^ n2)) by A87, FINSEQ_3:25;

then ((g | n1) ^ (g /^ n2)) . (i + 1) = ((g | n1) ^ (g /^ n2)) /. (i + 1) by PARTFUN1:def 6;

then reconsider z2 = ((g | n1) ^ (g /^ n2)) . (i + 1) as Element of FT ;

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

end;

suppose A88:
i < n1
; :: thesis: ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1

then A89:
i + 1 <= n1
by NAT_1:13;

i + 1 <= len (g | n1) by A78, A88, NAT_1:13;

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

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

A91: i < len g by A15, A88, XXREAL_0:2;

z1 = (g | n1) . i by A78, A84, A86, A88, FINSEQ_1:64

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

hence ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1 by A2, A84, A91, A90; :: thesis: verum

end;i + 1 <= len (g | n1) by A78, A88, NAT_1:13;

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

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

A91: i < len g by A15, A88, XXREAL_0:2;

z1 = (g | n1) . i by A78, A84, A86, A88, FINSEQ_1:64

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

hence ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1 by A2, A84, A91, A90; :: thesis: verum

suppose A92:
i >= n1
; :: thesis: ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1

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

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

then A94: (i -' n1) + n2 < ((len g) - n2) + n2 by XREAL_1:6;

A95: (len (g | n1)) + (i -' n1) = n1 + (i - n1) by A78, A92, XREAL_1:233

.= i ;

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

then A101: (i -' n1) + 1 <= len (g /^ n2) by A13, A76, XREAL_1:233;

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

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

(len (g | n1)) + ((i -' n1) + 1) = ((i - n1) + 1) + n1 by A78, A92, XREAL_1:233

.= i + 1 ;

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

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

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

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

hence ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1 by A2, A96, A103, A94; :: thesis: verum

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

then A94: (i -' n1) + n2 < ((len g) - n2) + n2 by XREAL_1:6;

A95: (len (g | n1)) + (i -' n1) = n1 + (i - n1) by A78, A92, XREAL_1:233

.= i ;

A96: now :: thesis: z1 = g . ((i -' n1) + n2)end;

i -' n1 < (len g) -' n2
by A13, A93, XREAL_1:233;per cases
( i > n1 or i = n1 )
by A92, XXREAL_0:1;

end;

suppose
i > n1
; :: thesis: z1 = g . ((i -' n1) + n2)

then A97:
i - n1 > 0
by XREAL_1:50;

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

then A98: 0 + 1 <= i -' n1 by A97, NAT_1:13;

then A99: i -' n1 in dom (g /^ n2) by A76, A93, FINSEQ_3:25;

thus z1 = (g /^ n2) . (i -' n1) by A76, A86, A93, A95, A98, FINSEQ_1:65

.= g . ((i -' n1) + n2) by A13, A99, RFINSEQ:def 1 ; :: thesis: verum

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

then A98: 0 + 1 <= i -' n1 by A97, NAT_1:13;

then A99: i -' n1 in dom (g /^ n2) by A76, A93, FINSEQ_3:25;

thus z1 = (g /^ n2) . (i -' n1) by A76, A86, A93, A95, A98, FINSEQ_1:65

.= g . ((i -' n1) + n2) by A13, A99, RFINSEQ:def 1 ; :: thesis: verum

suppose A100:
i = n1
; :: thesis: z1 = g . ((i -' n1) + n2)

hence z1 =
(g | n1) . n1
by A78, A84, A86, FINSEQ_1:64

.= g . (0 + n2) by A9, FINSEQ_3:112

.= g . ((i -' n1) + n2) by A100, XREAL_1:232 ;

:: thesis: verum

end;.= g . (0 + n2) by A9, FINSEQ_3:112

.= g . ((i -' n1) + n2) by A100, XREAL_1:232 ;

:: thesis: verum

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

then A101: (i -' n1) + 1 <= len (g /^ n2) by A13, A76, XREAL_1:233;

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

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

(len (g | n1)) + ((i -' n1) + 1) = ((i - n1) + 1) + n1 by A78, A92, XREAL_1:233

.= i + 1 ;

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

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

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

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

hence ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1 by A2, A96, A103, A94; :: thesis: verum

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

then rng ((g | n1) ^ (g /^ n2)) c= rng g by A104, XBOOLE_1:8;

then A105: rng ((g | n1) ^ (g /^ n2)) c= A by A4;

A106: ((len g) -' n2) + n2 = len g by A77;

A107: (len g) -' n2 in dom (g /^ n2) by A77, A76, A81, FINSEQ_3:25;

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

.= x2 by A6, A13, A107, A106, RFINSEQ:def 1 ;

then ((g | n1) ^ (g /^ n2)) . (len ((g | n1) ^ (g /^ n2))) = x2 by A15, A80, A77, FINSEQ_1:59;

then len g <= len ((g | n1) ^ (g /^ n2)) by A1, A79, A105, A83;

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

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

suppose A108:
n2 = len g
; :: thesis: contradiction

A109:
len (g /^ n2) = (len g) - n2
by A13, RFINSEQ:def 1;

A110: (g | n1) ^ (g /^ n2) is continuous

.= g | n1 by FINSEQ_1:34 ;

rng (g | n1) c= rng g by FINSEQ_5:19;

then A132: rng ((g | n1) ^ (g /^ n2)) c= A by A4, A131;

((g | n1) ^ (g /^ n2)) . (len ((g | n1) ^ (g /^ n2))) = x2 by A6, A9, A78, A108, A131, FINSEQ_3:112;

then len g <= len ((g | n1) ^ (g /^ n2)) by A1, A79, A132, A110;

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

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

end;A110: (g | n1) ^ (g /^ n2) is continuous

proof

A131: (g | n1) ^ (g /^ n2) =
(g | n1) ^ {}
by A108, FINSEQ_6:167
thus
len ((g | n1) ^ (g /^ n2)) >= 1
by A7, A11, A80, A108, FINSEQ_1:1; :: according to FINTOPO6:def 6 :: thesis: for i being Nat

for x1 being Element of FT st 1 <= i & i < len ((g | n1) ^ (g /^ n2)) & x1 = ((g | n1) ^ (g /^ n2)) . i holds

((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT x1

let i be Nat; :: thesis: for x1 being Element of FT st 1 <= i & i < len ((g | n1) ^ (g /^ n2)) & x1 = ((g | n1) ^ (g /^ n2)) . i holds

((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT x1

let z1 be Element of FT; :: thesis: ( 1 <= i & i < len ((g | n1) ^ (g /^ n2)) & z1 = ((g | n1) ^ (g /^ n2)) . i implies ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1 )

assume that

A111: 1 <= i and

A112: i < len ((g | n1) ^ (g /^ n2)) and

A113: z1 = ((g | n1) ^ (g /^ n2)) . i ; :: thesis: ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1

A114: i + 1 <= len ((g | n1) ^ (g /^ n2)) by A112, NAT_1:13;

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

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

then i + 1 in dom ((g | n1) ^ (g /^ n2)) by A114, FINSEQ_3:25;

then ((g | n1) ^ (g /^ n2)) . (i + 1) = ((g | n1) ^ (g /^ n2)) /. (i + 1) by PARTFUN1:def 6;

then reconsider z2 = ((g | n1) ^ (g /^ n2)) . (i + 1) as Element of FT ;

end;for x1 being Element of FT st 1 <= i & i < len ((g | n1) ^ (g /^ n2)) & x1 = ((g | n1) ^ (g /^ n2)) . i holds

((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT x1

let i be Nat; :: thesis: for x1 being Element of FT st 1 <= i & i < len ((g | n1) ^ (g /^ n2)) & x1 = ((g | n1) ^ (g /^ n2)) . i holds

((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT x1

let z1 be Element of FT; :: thesis: ( 1 <= i & i < len ((g | n1) ^ (g /^ n2)) & z1 = ((g | n1) ^ (g /^ n2)) . i implies ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1 )

assume that

A111: 1 <= i and

A112: i < len ((g | n1) ^ (g /^ n2)) and

A113: z1 = ((g | n1) ^ (g /^ n2)) . i ; :: thesis: ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1

A114: i + 1 <= len ((g | n1) ^ (g /^ n2)) by A112, NAT_1:13;

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

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

then i + 1 in dom ((g | n1) ^ (g /^ n2)) by A114, FINSEQ_3:25;

then ((g | n1) ^ (g /^ n2)) . (i + 1) = ((g | n1) ^ (g /^ n2)) /. (i + 1) by PARTFUN1:def 6;

then reconsider z2 = ((g | n1) ^ (g /^ n2)) . (i + 1) as Element of FT ;

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

end;

suppose A115:
i < n1
; :: thesis: ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1

then A116:
i + 1 <= n1
by NAT_1:13;

i + 1 <= len (g | n1) by A78, A115, NAT_1:13;

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

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

A118: i < len g by A15, A115, XXREAL_0:2;

z1 = (g | n1) . i by A78, A111, A113, A115, FINSEQ_1:64

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

hence ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1 by A2, A111, A118, A117; :: thesis: verum

end;i + 1 <= len (g | n1) by A78, A115, NAT_1:13;

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

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

A118: i < len g by A15, A115, XXREAL_0:2;

z1 = (g | n1) . i by A78, A111, A113, A115, FINSEQ_1:64

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

hence ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1 by A2, A111, A118, A117; :: thesis: verum

suppose A119:
i >= n1
; :: thesis: ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1

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

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

then A121: (i -' n1) + n2 < ((len g) - n2) + n2 by XREAL_1:6;

A122: (len (g | n1)) + (i -' n1) = n1 + (i - n1) by A78, A119, XREAL_1:233

.= i ;

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

then A128: (i -' n1) + 1 <= len (g /^ n2) by A13, A109, XREAL_1:233;

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

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

(len (g | n1)) + ((i -' n1) + 1) = ((i - n1) + 1) + n1 by A78, A119, XREAL_1:233

.= i + 1 ;

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

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

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

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

hence ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1 by A2, A123, A130, A121; :: thesis: verum

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

then A121: (i -' n1) + n2 < ((len g) - n2) + n2 by XREAL_1:6;

A122: (len (g | n1)) + (i -' n1) = n1 + (i - n1) by A78, A119, XREAL_1:233

.= i ;

A123: now :: thesis: z1 = g . ((i -' n1) + n2)end;

i -' n1 < (len g) -' n2
by A13, A120, XREAL_1:233;per cases
( i > n1 or i = n1 )
by A119, XXREAL_0:1;

end;

suppose
i > n1
; :: thesis: z1 = g . ((i -' n1) + n2)

then A124:
i - n1 > 0
by XREAL_1:50;

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

then A125: 0 + 1 <= i -' n1 by A124, NAT_1:13;

then A126: i -' n1 in dom (g /^ n2) by A109, A120, FINSEQ_3:25;

thus z1 = (g /^ n2) . (i -' n1) by A109, A113, A120, A122, A125, FINSEQ_1:65

.= g . ((i -' n1) + n2) by A13, A126, RFINSEQ:def 1 ; :: thesis: verum

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

then A125: 0 + 1 <= i -' n1 by A124, NAT_1:13;

then A126: i -' n1 in dom (g /^ n2) by A109, A120, FINSEQ_3:25;

thus z1 = (g /^ n2) . (i -' n1) by A109, A113, A120, A122, A125, FINSEQ_1:65

.= g . ((i -' n1) + n2) by A13, A126, RFINSEQ:def 1 ; :: thesis: verum

suppose A127:
i = n1
; :: thesis: z1 = g . ((i -' n1) + n2)

hence z1 =
(g | n1) . n1
by A78, A111, A113, FINSEQ_1:64

.= g . (0 + n2) by A9, FINSEQ_3:112

.= g . ((i -' n1) + n2) by A127, XREAL_1:232 ;

:: thesis: verum

end;.= g . (0 + n2) by A9, FINSEQ_3:112

.= g . ((i -' n1) + n2) by A127, XREAL_1:232 ;

:: thesis: verum

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

then A128: (i -' n1) + 1 <= len (g /^ n2) by A13, A109, XREAL_1:233;

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

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

(len (g | n1)) + ((i -' n1) + 1) = ((i - n1) + 1) + n1 by A78, A119, XREAL_1:233

.= i + 1 ;

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

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

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

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

hence ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1 by A2, A123, A130, A121; :: thesis: verum

.= g | n1 by FINSEQ_1:34 ;

rng (g | n1) c= rng g by FINSEQ_5:19;

then A132: rng ((g | n1) ^ (g /^ n2)) c= A by A4, A131;

((g | n1) ^ (g /^ n2)) . (len ((g | n1) ^ (g /^ n2))) = x2 by A6, A9, A78, A108, A131, FINSEQ_3:112;

then len g <= len ((g | n1) ^ (g /^ n2)) by A1, A79, A132, A110;

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

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