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 ;
A13: n2 <= len g by ;
A14: 1 <= n2 by ;
A15: n1 <= len g by ;
per cases ( n1 > n2 or n2 > n1 ) by ;
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 ;
A18: (len g) - n1 >= 0 by ;
then A19: (len g) -' n1 = (len g) - n1 by XREAL_0:def 2;
A20: len (g | n2) = n2 by ;
then A21: ((g | n2) ^ (g /^ n1)) . 1 = (g | n2) . 1 by
.= g . 1 by ;
A22: len ((g | n2) ^ (g /^ n1)) = (len (g | n2)) + (len (g /^ n1)) by FINSEQ_1:22
.= n2 + ((len g) - n1) by ;
per cases ( n1 < len g or n1 = len g ) by ;
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
proof
thus len ((g | n2) ^ (g /^ n1)) >= 1 by ; :: 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 ;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
1 < i + 1 by ;
then i + 1 in dom ((g | n2) ^ (g /^ n1)) by ;
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 z1
per cases ( i < n2 or i >= n2 ) ;
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 ;
then A32: z2 = (g | n2) . (i + 1) by
.= g . (i + 1) by ;
A33: i < len g by ;
z1 = (g | n2) . i by
.= g . i by ;
hence z2 in U_FT z1 by A2, A26, A33, A32; :: thesis: verum
end;
suppose A34: i >= n2 ; :: thesis: z2 in U_FT z1
i - n2 < (n2 + ((len g) - n1)) - n2 by ;
then A35: i -' n2 < (len g) - n1 by ;
then A36: (i -' n2) + n1 < ((len g) - n1) + n1 by XREAL_1:6;
A37: (len (g | n2)) + (i -' n2) = n2 + (i - n2) by
.= i ;
A38: now :: thesis: z1 = g . ((i -' n2) + n1)
per cases ( i > n2 or i = n2 ) by ;
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 ;
then A41: i -' n2 in dom (g /^ n1) by ;
thus z1 = (g /^ n1) . (i -' n2) by
.= g . ((i -' n2) + n1) by ; :: thesis: verum
end;
suppose A42: i = n2 ; :: thesis: z1 = g . ((i -' n2) + n1)
hence z1 = (g | n2) . n2 by
.= g . (0 + n1) by
.= g . ((i -' n2) + n1) by ;
:: thesis: verum
end;
end;
end;
i -' n2 < (len g) -' n1 by ;
then (i -' n2) + 1 <= (len g) -' n1 by NAT_1:13;
then A43: (i -' n2) + 1 <= len (g /^ n1) by ;
1 <= (i -' n2) + 1 by NAT_1:12;
then A44: (i -' n2) + 1 in dom (g /^ n1) by ;
(len (g | n2)) + ((i -' n2) + 1) = ((i - n2) + 1) + n2 by
.= i + 1 ;
then A45: z2 = (g /^ n1) . ((i -' n2) + 1) by
.= g . (((i -' n2) + 1) + n1) by
.= g . (((i -' n2) + n1) + 1) ;
1 <= (i -' n2) + n1 by ;
hence z2 in U_FT z1 by A2, A38, A45, A36; :: thesis: verum
end;
end;
end;
hence ((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT z1 ; :: thesis: verum
end;
A46: rng (g /^ n1) c= rng g by FINSEQ_5:33;
( rng ((g | n2) ^ (g /^ n1)) = (rng (g | n2)) \/ (rng (g /^ n1)) & rng (g | n2) c= rng g ) by ;
then A47: rng ((g | n2) ^ (g /^ n1)) c= rng g by ;
A48: ((len g) -' n1) + n1 = len g by A19;
A49: (len g) -' n1 in dom (g /^ n1) by ;
then ((g | n2) ^ (g /^ n1)) . ((len (g | n2)) + ((len g) -' n1)) = (g /^ n1) . ((len g) -' n1) by FINSEQ_1:def 7
.= x2 by ;
then ((g | n2) ^ (g /^ n1)) . (len ((g | n2) ^ (g /^ n1))) = x2 by ;
then len g <= len ((g | n2) ^ (g /^ n1)) by ;
then (len g) - n2 <= (n2 + ((len g) - n1)) - n2 by ;
hence contradiction by A16, XREAL_1:10; :: thesis: verum
end;
suppose A50: n1 = len g ; :: thesis: contradiction
A51: len (g /^ n1) = (len g) - n1 by ;
A52: (g | n2) ^ (g /^ n1) is continuous
proof
thus 1 <= len ((g | n2) ^ (g /^ n1)) by ; :: 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 ;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
1 < i + 1 by ;
then i + 1 in dom ((g | n2) ^ (g /^ n1)) by ;
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 ) ;
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 ;
then A59: z2 = (g | n2) . (i + 1) by
.= g . (i + 1) by ;
A60: i < len g by ;
z1 = (g | n2) . i by
.= g . i by ;
hence ((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT z1 by A2, A53, A60, A59; :: thesis: verum
end;
suppose A61: i >= n2 ; :: thesis: ((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT z1
i - n2 < (n2 + ((len g) - n1)) - n2 by ;
then A62: i -' n2 < (len g) - n1 by ;
then A63: (i -' n2) + n1 < ((len g) - n1) + n1 by XREAL_1:6;
A64: (len (g | n2)) + (i -' n2) = n2 + (i - n2) by
.= i ;
A65: now :: thesis: z1 = g . ((i -' n2) + n1)
per cases ( i > n2 or i = n2 ) by ;
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 ;
then A68: i -' n2 in dom (g /^ n1) by ;
thus z1 = (g /^ n1) . (i -' n2) by
.= g . ((i -' n2) + n1) by ; :: thesis: verum
end;
suppose A69: i = n2 ; :: thesis: z1 = g . ((i -' n2) + n1)
hence z1 = (g | n2) . n2 by
.= g . (0 + n1) by
.= g . ((i -' n2) + n1) by ;
:: thesis: verum
end;
end;
end;
i -' n2 < (len g) -' n1 by ;
then (i -' n2) + 1 <= (len g) -' n1 by NAT_1:13;
then A70: (i -' n2) + 1 <= len (g /^ n1) by ;
1 <= (i -' n2) + 1 by NAT_1:12;
then A71: (i -' n2) + 1 in dom (g /^ n1) by ;
(len (g | n2)) + ((i -' n2) + 1) = ((i - n2) + 1) + n2 by
.= i + 1 ;
then A72: z2 = (g /^ n1) . ((i -' n2) + 1) by
.= g . (((i -' n2) + 1) + n1) by
.= g . (((i -' n2) + n1) + 1) ;
1 <= (i -' n2) + n1 by ;
hence ((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT z1 by A2, A65, A72, A63; :: thesis: verum
end;
end;
end;
A73: rng (g | n2) c= rng g by FINSEQ_5:19;
A74: (g | n2) ^ (g /^ n1) = (g | n2) ^ {} by
.= g | n2 by FINSEQ_1:34 ;
then ((g | n2) ^ (g /^ n1)) . (len ((g | n2) ^ (g /^ n1))) = x2 by ;
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 ;
hence contradiction by A16, XREAL_1:10; :: thesis: verum
end;
end;
end;
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 ;
(len g) - n2 >= 0 by ;
then A77: (len g) -' n2 = (len g) - n2 by XREAL_0:def 2;
A78: len (g | n1) = n1 by ;
then A79: ((g | n1) ^ (g /^ n2)) . 1 = (g | n1) . 1 by
.= x1 by ;
A80: len ((g | n1) ^ (g /^ n2)) = (len (g | n1)) + (len (g /^ n2)) by FINSEQ_1:22
.= n1 + ((len g) - n2) by ;
per cases ( n2 < len g or n2 = len g ) by ;
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
proof
thus len ((g | n1) ^ (g /^ n2)) >= 1 by ; :: 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 ;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
1 < i + 1 by ;
then i + 1 in dom ((g | n1) ^ (g /^ n2)) by ;
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 ) ;
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 ;
then A90: z2 = (g | n1) . (i + 1) by
.= g . (i + 1) by ;
A91: i < len g by ;
z1 = (g | n1) . i by
.= g . i by ;
hence ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1 by A2, A84, A91, A90; :: thesis: verum
end;
suppose A92: i >= n1 ; :: thesis: ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1
i - n1 < (n1 + ((len g) - n2)) - n1 by ;
then A93: i -' n1 < (len g) - n2 by ;
then A94: (i -' n1) + n2 < ((len g) - n2) + n2 by XREAL_1:6;
A95: (len (g | n1)) + (i -' n1) = n1 + (i - n1) by
.= i ;
A96: now :: thesis: z1 = g . ((i -' n1) + n2)
per cases ( i > n1 or i = n1 ) by ;
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 ;
then A99: i -' n1 in dom (g /^ n2) by ;
thus z1 = (g /^ n2) . (i -' n1) by
.= g . ((i -' n1) + n2) by ; :: thesis: verum
end;
suppose A100: i = n1 ; :: thesis: z1 = g . ((i -' n1) + n2)
hence z1 = (g | n1) . n1 by
.= g . (0 + n2) by
.= g . ((i -' n1) + n2) by ;
:: thesis: verum
end;
end;
end;
i -' n1 < (len g) -' n2 by ;
then (i -' n1) + 1 <= (len g) -' n2 by NAT_1:13;
then A101: (i -' n1) + 1 <= len (g /^ n2) by ;
1 <= (i -' n1) + 1 by NAT_1:12;
then A102: (i -' n1) + 1 in dom (g /^ n2) by ;
(len (g | n1)) + ((i -' n1) + 1) = ((i - n1) + 1) + n1 by
.= i + 1 ;
then A103: z2 = (g /^ n2) . ((i -' n1) + 1) by
.= g . (((i -' n1) + 1) + n2) by
.= g . (((i -' n1) + n2) + 1) ;
1 <= (i -' n1) + n2 by ;
hence ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1 by A2, A96, A103, A94; :: thesis: verum
end;
end;
end;
A104: rng (g /^ n2) c= rng g by FINSEQ_5:33;
( rng ((g | n1) ^ (g /^ n2)) = (rng (g | n1)) \/ (rng (g /^ n2)) & rng (g | n1) c= rng g ) by ;
then rng ((g | n1) ^ (g /^ n2)) c= rng g by ;
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 ;
then ((g | n1) ^ (g /^ n2)) . ((len (g | n1)) + ((len g) -' n2)) = (g /^ n2) . ((len g) -' n2) by FINSEQ_1:def 7
.= x2 by ;
then ((g | n1) ^ (g /^ n2)) . (len ((g | n1) ^ (g /^ n2))) = x2 by ;
then len g <= len ((g | n1) ^ (g /^ n2)) by A1, A79, A105, A83;
then (len g) - n1 <= (n1 + ((len g) - n2)) - n1 by ;
hence contradiction by A75, XREAL_1:10; :: thesis: verum
end;
suppose A108: n2 = len g ; :: thesis: contradiction
A109: len (g /^ n2) = (len g) - n2 by ;
A110: (g | n1) ^ (g /^ n2) is continuous
proof
thus len ((g | n1) ^ (g /^ n2)) >= 1 by ; :: 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 ;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
1 < i + 1 by ;
then i + 1 in dom ((g | n1) ^ (g /^ n2)) by ;
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 ) ;
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 ;
then A117: z2 = (g | n1) . (i + 1) by
.= g . (i + 1) by ;
A118: i < len g by ;
z1 = (g | n1) . i by
.= g . i by ;
hence ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1 by ; :: thesis: verum
end;
suppose A119: i >= n1 ; :: thesis: ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1
i - n1 < (n1 + ((len g) - n2)) - n1 by ;
then A120: i -' n1 < (len g) - n2 by ;
then A121: (i -' n1) + n2 < ((len g) - n2) + n2 by XREAL_1:6;
A122: (len (g | n1)) + (i -' n1) = n1 + (i - n1) by
.= i ;
A123: now :: thesis: z1 = g . ((i -' n1) + n2)
per cases ( i > n1 or i = n1 ) by ;
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 ;
then A126: i -' n1 in dom (g /^ n2) by ;
thus z1 = (g /^ n2) . (i -' n1) by
.= g . ((i -' n1) + n2) by ; :: thesis: verum
end;
suppose A127: i = n1 ; :: thesis: z1 = g . ((i -' n1) + n2)
hence z1 = (g | n1) . n1 by
.= g . (0 + n2) by
.= g . ((i -' n1) + n2) by ;
:: thesis: verum
end;
end;
end;
i -' n1 < (len g) -' n2 by ;
then (i -' n1) + 1 <= (len g) -' n2 by NAT_1:13;
then A128: (i -' n1) + 1 <= len (g /^ n2) by ;
1 <= (i -' n1) + 1 by NAT_1:12;
then A129: (i -' n1) + 1 in dom (g /^ n2) by ;
(len (g | n1)) + ((i -' n1) + 1) = ((i - n1) + 1) + n1 by
.= i + 1 ;
then A130: z2 = (g /^ n2) . ((i -' n1) + 1) by
.= g . (((i -' n1) + 1) + n2) by
.= g . (((i -' n1) + n2) + 1) ;
1 <= (i -' n1) + n2 by ;
hence ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1 by ; :: thesis: verum
end;
end;
end;
A131: (g | n1) ^ (g /^ n2) = (g | n1) ^ {} by
.= 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 ;
((g | n1) ^ (g /^ n2)) . (len ((g | n1) ^ (g /^ n2))) = x2 by ;
then len g <= len ((g | n1) ^ (g /^ n2)) by ;
then (len g) - n1 <= (n1 + ((len g) - n2)) - n1 by ;
hence contradiction by A75, XREAL_1:10; :: thesis: verum
end;
end;
end;
end;