let f, g be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st f is being_S-Seq & p in L~ f & p <> f . ((Index (p,f)) + 1) & g = <*p*> ^ (mid (f,((Index (p,f)) + 1),(len f))) holds

g is_S-Seq_joining p,f /. (len f)

let p be Point of (TOP-REAL 2); :: thesis: ( f is being_S-Seq & p in L~ f & p <> f . ((Index (p,f)) + 1) & g = <*p*> ^ (mid (f,((Index (p,f)) + 1),(len f))) implies g is_S-Seq_joining p,f /. (len f) )

assume that

A1: f is being_S-Seq and

A2: p in L~ f and

A3: p <> f . ((Index (p,f)) + 1) and

A4: g = <*p*> ^ (mid (f,((Index (p,f)) + 1),(len f))) ; :: thesis: g is_S-Seq_joining p,f /. (len f)

len g = (len <*p*>) + (len (mid (f,((Index (p,f)) + 1),(len f)))) by A4, FINSEQ_1:22;

then A5: len g = 1 + (len (mid (f,((Index (p,f)) + 1),(len f)))) by FINSEQ_1:39;

consider i being Nat such that

1 <= i and

A6: i + 1 <= len f and

p in LSeg (f,i) by A2, SPPOL_2:13;

1 <= 1 + i by NAT_1:12;

then A7: 1 <= len f by A6, XXREAL_0:2;

A8: for j1, j2 being Nat st j1 + 1 < j2 holds

LSeg (g,j1) misses LSeg (g,j2)

then A17: (Index (p,f)) + 1 <= len f by NAT_1:13;

(Index (p,f)) + 1 <= len f by A16, NAT_1:13;

then A18: ((Index (p,f)) + 1) - (Index (p,f)) <= (len f) - (Index (p,f)) by XREAL_1:9;

then A19: 1 - 1 <= ((len f) - (Index (p,f))) - 1 by XREAL_1:9;

then A20: (len f) -' ((Index (p,f)) + 1) = (len f) - ((Index (p,f)) + 1) by XREAL_0:def 2

.= ((len f) - (Index (p,f))) - 1 ;

A21: 0 + 1 <= (Index (p,f)) + 1 by NAT_1:11;

then A22: len (mid (f,((Index (p,f)) + 1),(len f))) = ((len f) -' ((Index (p,f)) + 1)) + 1 by A7, A17, FINSEQ_6:118;

A23: for j being Nat st 1 <= j & j + 2 <= len g holds

(LSeg (g,j)) /\ (LSeg (g,(j + 1))) = {(g /. (j + 1))}

.= 1 + (len (mid (f,((Index (p,f)) + 1),(len f)))) by FINSEQ_1:39 ;

then A47: len g = 1 + (((len f) - ((Index (p,f)) + 1)) + 1) by A19, A22, XREAL_0:def 2

.= 1 + ((len f) - (Index (p,f))) ;

then A48: (len g) -' 1 = (len g) - 1 by A18, XREAL_0:def 2;

then A49: (len g) -' 1 in dom (mid (f,((Index (p,f)) + 1),(len f))) by A18, A22, A47, A20, FINSEQ_3:25;

A50: (len f) - (Index (p,f)) >= 0 by A2, Th8, XREAL_1:50;

then A51: (len f) - (Index (p,f)) = (len f) -' (Index (p,f)) by XREAL_0:def 2;

then A52: (mid (f,((Index (p,f)) + 1),(len f))) . ((len f) -' (Index (p,f))) = f . ((((len f) -' (Index (p,f))) + ((Index (p,f)) + 1)) -' 1) by A7, A18, A17, A21, A22, A20, FINSEQ_6:118;

A53: (len g) -' 1 = (len f) -' (Index (p,f)) by A47, A48, XREAL_0:def 2;

for x1, x2 being object st x1 in dom g & x2 in dom g & g . x1 = g . x2 holds

x1 = x2

A101: ((len g) - 1) + 1 >= 1 + 1 by A18, A47, XREAL_1:6;

A102: ((len f) -' ((Index (p,f)) + 1)) + 1 = (len f) - (Index (p,f)) by A20;

for j being Nat st 1 <= j & j + 1 <= len g & not (g /. j) `1 = (g /. (j + 1)) `1 holds

(g /. j) `2 = (g /. (j + 1)) `2

then A112: g is being_S-Seq by A101, A100, TOPREAL1:def 8;

A113: ((len f) -' (Index (p,f))) + ((Index (p,f)) + 1) = ((len f) - (Index (p,f))) + ((Index (p,f)) + 1) by A50, XREAL_0:def 2

.= (len f) + 1 ;

1 + ((len g) -' 1) = 1 + ((len g) - 1) by A46, XREAL_0:def 2

.= len g ;

then g . (len g) = g . ((len <*p*>) + ((len g) -' 1)) by FINSEQ_1:39

.= (mid (f,((Index (p,f)) + 1),(len f))) . ((len g) -' 1) by A4, A49, FINSEQ_1:def 7 ;

then g . (len g) = f . (len f) by A47, A48, A52, A113, NAT_D:34;

then A114: g . (len g) = f /. (len f) by A7, FINSEQ_4:15;

g . 1 = p by A4, FINSEQ_1:41;

hence g is_S-Seq_joining p,f /. (len f) by A112, A114; :: thesis: verum

g is_S-Seq_joining p,f /. (len f)

let p be Point of (TOP-REAL 2); :: thesis: ( f is being_S-Seq & p in L~ f & p <> f . ((Index (p,f)) + 1) & g = <*p*> ^ (mid (f,((Index (p,f)) + 1),(len f))) implies g is_S-Seq_joining p,f /. (len f) )

assume that

A1: f is being_S-Seq and

A2: p in L~ f and

A3: p <> f . ((Index (p,f)) + 1) and

A4: g = <*p*> ^ (mid (f,((Index (p,f)) + 1),(len f))) ; :: thesis: g is_S-Seq_joining p,f /. (len f)

len g = (len <*p*>) + (len (mid (f,((Index (p,f)) + 1),(len f)))) by A4, FINSEQ_1:22;

then A5: len g = 1 + (len (mid (f,((Index (p,f)) + 1),(len f)))) by FINSEQ_1:39;

consider i being Nat such that

1 <= i and

A6: i + 1 <= len f and

p in LSeg (f,i) by A2, SPPOL_2:13;

1 <= 1 + i by NAT_1:12;

then A7: 1 <= len f by A6, XXREAL_0:2;

A8: for j1, j2 being Nat st j1 + 1 < j2 holds

LSeg (g,j1) misses LSeg (g,j2)

proof

A16:
Index (p,f) < len f
by A2, Th8;
let j1, j2 be Nat; :: thesis: ( j1 + 1 < j2 implies LSeg (g,j1) misses LSeg (g,j2) )

assume A9: j1 + 1 < j2 ; :: thesis: LSeg (g,j1) misses LSeg (g,j2)

A10: ( j1 = 0 or j1 >= 0 + 1 ) by NAT_1:13;

end;assume A9: j1 + 1 < j2 ; :: thesis: LSeg (g,j1) misses LSeg (g,j2)

A10: ( j1 = 0 or j1 >= 0 + 1 ) by NAT_1:13;

now :: thesis: ( ( j1 = 0 & LSeg (g,j1) misses LSeg (g,j2) ) or ( ( j1 = 1 or j1 > 1 ) & j2 + 1 <= len g & LSeg (g,j1) misses LSeg (g,j2) ) or ( j2 + 1 > len g & LSeg (g,j1) misses LSeg (g,j2) ) )end;

hence
LSeg (g,j1) misses LSeg (g,j2)
; :: thesis: verumper cases
( j1 = 0 or ( ( j1 = 1 or j1 > 1 ) & j2 + 1 <= len g ) or j2 + 1 > len g )
by A10, XXREAL_0:1;

end;

case
j1 = 0
; :: thesis: LSeg (g,j1) misses LSeg (g,j2)

then
LSeg (g,j1) = {}
by TOPREAL1:def 3;

then (LSeg (g,j1)) /\ (LSeg (g,j2)) = {} ;

hence LSeg (g,j1) misses LSeg (g,j2) by XBOOLE_0:def 7; :: thesis: verum

end;then (LSeg (g,j1)) /\ (LSeg (g,j2)) = {} ;

hence LSeg (g,j1) misses LSeg (g,j2) by XBOOLE_0:def 7; :: thesis: verum

case that A11:
( j1 = 1 or j1 > 1 )
and

A12: j2 + 1 <= len g ; :: thesis: LSeg (g,j1) misses LSeg (g,j2)

A12: j2 + 1 <= len g ; :: thesis: LSeg (g,j1) misses LSeg (g,j2)

1 < j1 + 1
by A11, NAT_1:13;

then 1 <= j2 by A9, XXREAL_0:2;

then A13: LSeg (g,j2) c= LSeg (f,(((Index (p,f)) + j2) -' 1)) by A2, A4, A12, Th16;

1 <= (Index (p,f)) + j1 by A2, Th8, NAT_1:12;

then 1 - 1 <= ((Index (p,f)) + j1) - 1 by XREAL_1:9;

then A14: ((Index (p,f)) + j1) - 1 = ((Index (p,f)) + j1) -' 1 by XREAL_0:def 2;

(Index (p,f)) + (j1 + 1) < (Index (p,f)) + j2 by A9, XREAL_1:6;

then (((Index (p,f)) + j1) + 1) - 1 < ((Index (p,f)) + j2) - 1 by XREAL_1:9;

then (((Index (p,f)) + j1) -' 1) + 1 < ((Index (p,f)) + j2) -' 1 by A14, XREAL_0:def 2;

then LSeg (f,(((Index (p,f)) + j1) -' 1)) misses LSeg (f,(((Index (p,f)) + j2) -' 1)) by A1, TOPREAL1:def 7;

then A15: (LSeg (f,(((Index (p,f)) + j1) -' 1))) /\ (LSeg (f,(((Index (p,f)) + j2) -' 1))) = {} by XBOOLE_0:def 7;

j2 < len g by A12, NAT_1:13;

then j1 + 1 <= len g by A9, XXREAL_0:2;

then LSeg (g,j1) c= LSeg (f,(((Index (p,f)) + j1) -' 1)) by A2, A4, A11, Th16;

then (LSeg (g,j1)) /\ (LSeg (g,j2)) = {} by A13, A15, XBOOLE_1:3, XBOOLE_1:27;

hence LSeg (g,j1) misses LSeg (g,j2) by XBOOLE_0:def 7; :: thesis: verum

end;then 1 <= j2 by A9, XXREAL_0:2;

then A13: LSeg (g,j2) c= LSeg (f,(((Index (p,f)) + j2) -' 1)) by A2, A4, A12, Th16;

1 <= (Index (p,f)) + j1 by A2, Th8, NAT_1:12;

then 1 - 1 <= ((Index (p,f)) + j1) - 1 by XREAL_1:9;

then A14: ((Index (p,f)) + j1) - 1 = ((Index (p,f)) + j1) -' 1 by XREAL_0:def 2;

(Index (p,f)) + (j1 + 1) < (Index (p,f)) + j2 by A9, XREAL_1:6;

then (((Index (p,f)) + j1) + 1) - 1 < ((Index (p,f)) + j2) - 1 by XREAL_1:9;

then (((Index (p,f)) + j1) -' 1) + 1 < ((Index (p,f)) + j2) -' 1 by A14, XREAL_0:def 2;

then LSeg (f,(((Index (p,f)) + j1) -' 1)) misses LSeg (f,(((Index (p,f)) + j2) -' 1)) by A1, TOPREAL1:def 7;

then A15: (LSeg (f,(((Index (p,f)) + j1) -' 1))) /\ (LSeg (f,(((Index (p,f)) + j2) -' 1))) = {} by XBOOLE_0:def 7;

j2 < len g by A12, NAT_1:13;

then j1 + 1 <= len g by A9, XXREAL_0:2;

then LSeg (g,j1) c= LSeg (f,(((Index (p,f)) + j1) -' 1)) by A2, A4, A11, Th16;

then (LSeg (g,j1)) /\ (LSeg (g,j2)) = {} by A13, A15, XBOOLE_1:3, XBOOLE_1:27;

hence LSeg (g,j1) misses LSeg (g,j2) by XBOOLE_0:def 7; :: thesis: verum

then A17: (Index (p,f)) + 1 <= len f by NAT_1:13;

(Index (p,f)) + 1 <= len f by A16, NAT_1:13;

then A18: ((Index (p,f)) + 1) - (Index (p,f)) <= (len f) - (Index (p,f)) by XREAL_1:9;

then A19: 1 - 1 <= ((len f) - (Index (p,f))) - 1 by XREAL_1:9;

then A20: (len f) -' ((Index (p,f)) + 1) = (len f) - ((Index (p,f)) + 1) by XREAL_0:def 2

.= ((len f) - (Index (p,f))) - 1 ;

A21: 0 + 1 <= (Index (p,f)) + 1 by NAT_1:11;

then A22: len (mid (f,((Index (p,f)) + 1),(len f))) = ((len f) -' ((Index (p,f)) + 1)) + 1 by A7, A17, FINSEQ_6:118;

A23: for j being Nat st 1 <= j & j + 2 <= len g holds

(LSeg (g,j)) /\ (LSeg (g,(j + 1))) = {(g /. (j + 1))}

proof

A46: len g =
(len <*p*>) + (len (mid (f,((Index (p,f)) + 1),(len f))))
by A4, FINSEQ_1:22
let j be Nat; :: thesis: ( 1 <= j & j + 2 <= len g implies (LSeg (g,j)) /\ (LSeg (g,(j + 1))) = {(g /. (j + 1))} )

assume that

A24: 1 <= j and

A25: j + 2 <= len g ; :: thesis: (LSeg (g,j)) /\ (LSeg (g,(j + 1))) = {(g /. (j + 1))}

A26: j + 2 = (j + 1) + 1 ;

then A27: j + 1 <= len g by A25, NAT_1:13;

then A28: LSeg (g,j) c= LSeg (f,(((Index (p,f)) + j) -' 1)) by A2, A4, A24, Th16;

1 <= j + 1 by A24, NAT_1:13;

then LSeg (g,(j + 1)) c= LSeg (f,(((Index (p,f)) + (j + 1)) -' 1)) by A2, A4, A25, A26, Th16;

then A29: (LSeg (g,j)) /\ (LSeg (g,(j + 1))) c= (LSeg (f,(((Index (p,f)) + j) -' 1))) /\ (LSeg (f,(((Index (p,f)) + (j + 1)) -' 1))) by A28, XBOOLE_1:27;

A30: 1 <= Index (p,f) by A2, Th8;

1 <= Index (p,f) by A2, Th8;

then 1 + 1 <= (Index (p,f)) + j by A24, XREAL_1:7;

then 1 <= ((Index (p,f)) + j) - 1 by XREAL_1:19;

then A31: 1 <= ((Index (p,f)) + j) -' 1 by NAT_D:39;

1 <= (Index (p,f)) + j by A2, Th8, NAT_1:12;

then A32: 1 - 1 <= ((Index (p,f)) + j) - 1 by XREAL_1:9;

((j + 1) + 1) - 1 <= (1 + (len (mid (f,((Index (p,f)) + 1),(len f))))) - 1 by A5, A25, XREAL_1:9;

then A33: (j + 1) + (Index (p,f)) <= ((len f) - (Index (p,f))) + (Index (p,f)) by A22, A20, XREAL_1:6;

then ((Index (p,f)) + j) + 1 <= len f ;

then ((Index (p,f)) + (j - 1)) + 1 <= len f by NAT_D:46;

then A34: (((Index (p,f)) + j) -' 1) + 1 <= len f by A32, XREAL_0:def 2;

(((Index (p,f)) + j) - 1) + (1 + 1) <= len f by A33;

then (((Index (p,f)) + j) -' 1) + 2 <= len f by A32, XREAL_0:def 2;

then A35: {(f /. ((((Index (p,f)) + j) -' 1) + 1))} = (LSeg (f,(((Index (p,f)) + j) -' 1))) /\ (LSeg (f,((((Index (p,f)) + j) -' 1) + 1))) by A1, A31, TOPREAL1:def 6;

A36: 1 < j + 1 by A24, NAT_1:13;

then A37: g /. (j + 1) = g . (j + 1) by A27, FINSEQ_4:15;

A38: g /. (j + 1) in LSeg ((g /. (j + 1)),(g /. ((j + 1) + 1))) by RLTOPSP1:68;

g /. (j + 1) in LSeg ((g /. j),(g /. (j + 1))) by RLTOPSP1:68;

then A39: g /. (j + 1) in (LSeg ((g /. j),(g /. (j + 1)))) /\ (LSeg ((g /. (j + 1)),(g /. ((j + 1) + 1)))) by A38, XBOOLE_0:def 4;

A40: LSeg (g,j) = LSeg ((g /. j),(g /. (j + 1))) by A24, A27, TOPREAL1:def 3;

LSeg ((g /. (j + 1)),(g /. ((j + 1) + 1))) = LSeg (g,(j + 1)) by A25, A36, TOPREAL1:def 3;

then A41: {(g /. (j + 1))} c= (LSeg (g,j)) /\ (LSeg (g,(j + 1))) by A40, A39, ZFMISC_1:31;

A42: j + 1 = ((j + 1) - 1) + 1

.= ((j + 1) -' 1) + 1 by A36, XREAL_1:233 ;

then A43: j + 1 = (len <*p*>) + ((j + 1) -' 1) by FINSEQ_1:39;

A44: (j + 1) -' 1 <= len (mid (f,((Index (p,f)) + 1),(len f))) by A5, A27, A42, XREAL_1:6;

then (j + 1) -' 1 in dom (mid (f,((Index (p,f)) + 1),(len f))) by A24, A42, FINSEQ_3:25;

then g . (j + 1) = (mid (f,((Index (p,f)) + 1),(len f))) . ((j + 1) -' 1) by A4, A43, FINSEQ_1:def 7

.= f . ((((j + 1) -' 1) + ((Index (p,f)) + 1)) -' 1) by A7, A17, A21, A24, A42, A44, FINSEQ_6:118

.= f . (((((j + 1) -' 1) + 1) + (Index (p,f))) -' 1)

.= f . (((j + 1) + (Index (p,f))) -' 1) by A36, XREAL_1:235

.= f . ((((Index (p,f)) + j) + 1) -' 1)

.= f . ((Index (p,f)) + j) by NAT_D:34

.= f . ((((Index (p,f)) + j) -' 1) + 1) by A30, NAT_1:12, XREAL_1:235 ;

then A45: f /. ((((Index (p,f)) + j) -' 1) + 1) = g /. (j + 1) by A37, A34, FINSEQ_4:15, NAT_1:11;

((Index (p,f)) + (j + 1)) -' 1 = (((Index (p,f)) + j) + 1) - 1 by NAT_1:11, XREAL_1:233

.= (((Index (p,f)) + j) - 1) + 1

.= (((Index (p,f)) + j) -' 1) + 1 by A30, NAT_1:12, XREAL_1:233 ;

hence (LSeg (g,j)) /\ (LSeg (g,(j + 1))) = {(g /. (j + 1))} by A29, A35, A45, A41, XBOOLE_0:def 10; :: thesis: verum

end;assume that

A24: 1 <= j and

A25: j + 2 <= len g ; :: thesis: (LSeg (g,j)) /\ (LSeg (g,(j + 1))) = {(g /. (j + 1))}

A26: j + 2 = (j + 1) + 1 ;

then A27: j + 1 <= len g by A25, NAT_1:13;

then A28: LSeg (g,j) c= LSeg (f,(((Index (p,f)) + j) -' 1)) by A2, A4, A24, Th16;

1 <= j + 1 by A24, NAT_1:13;

then LSeg (g,(j + 1)) c= LSeg (f,(((Index (p,f)) + (j + 1)) -' 1)) by A2, A4, A25, A26, Th16;

then A29: (LSeg (g,j)) /\ (LSeg (g,(j + 1))) c= (LSeg (f,(((Index (p,f)) + j) -' 1))) /\ (LSeg (f,(((Index (p,f)) + (j + 1)) -' 1))) by A28, XBOOLE_1:27;

A30: 1 <= Index (p,f) by A2, Th8;

1 <= Index (p,f) by A2, Th8;

then 1 + 1 <= (Index (p,f)) + j by A24, XREAL_1:7;

then 1 <= ((Index (p,f)) + j) - 1 by XREAL_1:19;

then A31: 1 <= ((Index (p,f)) + j) -' 1 by NAT_D:39;

1 <= (Index (p,f)) + j by A2, Th8, NAT_1:12;

then A32: 1 - 1 <= ((Index (p,f)) + j) - 1 by XREAL_1:9;

((j + 1) + 1) - 1 <= (1 + (len (mid (f,((Index (p,f)) + 1),(len f))))) - 1 by A5, A25, XREAL_1:9;

then A33: (j + 1) + (Index (p,f)) <= ((len f) - (Index (p,f))) + (Index (p,f)) by A22, A20, XREAL_1:6;

then ((Index (p,f)) + j) + 1 <= len f ;

then ((Index (p,f)) + (j - 1)) + 1 <= len f by NAT_D:46;

then A34: (((Index (p,f)) + j) -' 1) + 1 <= len f by A32, XREAL_0:def 2;

(((Index (p,f)) + j) - 1) + (1 + 1) <= len f by A33;

then (((Index (p,f)) + j) -' 1) + 2 <= len f by A32, XREAL_0:def 2;

then A35: {(f /. ((((Index (p,f)) + j) -' 1) + 1))} = (LSeg (f,(((Index (p,f)) + j) -' 1))) /\ (LSeg (f,((((Index (p,f)) + j) -' 1) + 1))) by A1, A31, TOPREAL1:def 6;

A36: 1 < j + 1 by A24, NAT_1:13;

then A37: g /. (j + 1) = g . (j + 1) by A27, FINSEQ_4:15;

A38: g /. (j + 1) in LSeg ((g /. (j + 1)),(g /. ((j + 1) + 1))) by RLTOPSP1:68;

g /. (j + 1) in LSeg ((g /. j),(g /. (j + 1))) by RLTOPSP1:68;

then A39: g /. (j + 1) in (LSeg ((g /. j),(g /. (j + 1)))) /\ (LSeg ((g /. (j + 1)),(g /. ((j + 1) + 1)))) by A38, XBOOLE_0:def 4;

A40: LSeg (g,j) = LSeg ((g /. j),(g /. (j + 1))) by A24, A27, TOPREAL1:def 3;

LSeg ((g /. (j + 1)),(g /. ((j + 1) + 1))) = LSeg (g,(j + 1)) by A25, A36, TOPREAL1:def 3;

then A41: {(g /. (j + 1))} c= (LSeg (g,j)) /\ (LSeg (g,(j + 1))) by A40, A39, ZFMISC_1:31;

A42: j + 1 = ((j + 1) - 1) + 1

.= ((j + 1) -' 1) + 1 by A36, XREAL_1:233 ;

then A43: j + 1 = (len <*p*>) + ((j + 1) -' 1) by FINSEQ_1:39;

A44: (j + 1) -' 1 <= len (mid (f,((Index (p,f)) + 1),(len f))) by A5, A27, A42, XREAL_1:6;

then (j + 1) -' 1 in dom (mid (f,((Index (p,f)) + 1),(len f))) by A24, A42, FINSEQ_3:25;

then g . (j + 1) = (mid (f,((Index (p,f)) + 1),(len f))) . ((j + 1) -' 1) by A4, A43, FINSEQ_1:def 7

.= f . ((((j + 1) -' 1) + ((Index (p,f)) + 1)) -' 1) by A7, A17, A21, A24, A42, A44, FINSEQ_6:118

.= f . (((((j + 1) -' 1) + 1) + (Index (p,f))) -' 1)

.= f . (((j + 1) + (Index (p,f))) -' 1) by A36, XREAL_1:235

.= f . ((((Index (p,f)) + j) + 1) -' 1)

.= f . ((Index (p,f)) + j) by NAT_D:34

.= f . ((((Index (p,f)) + j) -' 1) + 1) by A30, NAT_1:12, XREAL_1:235 ;

then A45: f /. ((((Index (p,f)) + j) -' 1) + 1) = g /. (j + 1) by A37, A34, FINSEQ_4:15, NAT_1:11;

((Index (p,f)) + (j + 1)) -' 1 = (((Index (p,f)) + j) + 1) - 1 by NAT_1:11, XREAL_1:233

.= (((Index (p,f)) + j) - 1) + 1

.= (((Index (p,f)) + j) -' 1) + 1 by A30, NAT_1:12, XREAL_1:233 ;

hence (LSeg (g,j)) /\ (LSeg (g,(j + 1))) = {(g /. (j + 1))} by A29, A35, A45, A41, XBOOLE_0:def 10; :: thesis: verum

.= 1 + (len (mid (f,((Index (p,f)) + 1),(len f)))) by FINSEQ_1:39 ;

then A47: len g = 1 + (((len f) - ((Index (p,f)) + 1)) + 1) by A19, A22, XREAL_0:def 2

.= 1 + ((len f) - (Index (p,f))) ;

then A48: (len g) -' 1 = (len g) - 1 by A18, XREAL_0:def 2;

then A49: (len g) -' 1 in dom (mid (f,((Index (p,f)) + 1),(len f))) by A18, A22, A47, A20, FINSEQ_3:25;

A50: (len f) - (Index (p,f)) >= 0 by A2, Th8, XREAL_1:50;

then A51: (len f) - (Index (p,f)) = (len f) -' (Index (p,f)) by XREAL_0:def 2;

then A52: (mid (f,((Index (p,f)) + 1),(len f))) . ((len f) -' (Index (p,f))) = f . ((((len f) -' (Index (p,f))) + ((Index (p,f)) + 1)) -' 1) by A7, A18, A17, A21, A22, A20, FINSEQ_6:118;

A53: (len g) -' 1 = (len f) -' (Index (p,f)) by A47, A48, XREAL_0:def 2;

for x1, x2 being object st x1 in dom g & x2 in dom g & g . x1 = g . x2 holds

x1 = x2

proof

then A100:
g is one-to-one
by FUNCT_1:def 4;
let x1, x2 be object ; :: thesis: ( x1 in dom g & x2 in dom g & g . x1 = g . x2 implies x1 = x2 )

assume that

A54: x1 in dom g and

A55: x2 in dom g and

A56: g . x1 = g . x2 ; :: thesis: x1 = x2

reconsider n1 = x1, n2 = x2 as Element of NAT by A54, A55;

A57: n1 <= len g by A54, FINSEQ_3:25;

A58: 1 <= n2 by A55, FINSEQ_3:25;

A59: n2 <= len g by A55, FINSEQ_3:25;

A60: 1 <= n1 by A54, FINSEQ_3:25;

end;assume that

A54: x1 in dom g and

A55: x2 in dom g and

A56: g . x1 = g . x2 ; :: thesis: x1 = x2

reconsider n1 = x1, n2 = x2 as Element of NAT by A54, A55;

A57: n1 <= len g by A54, FINSEQ_3:25;

A58: 1 <= n2 by A55, FINSEQ_3:25;

A59: n2 <= len g by A55, FINSEQ_3:25;

A60: 1 <= n1 by A54, FINSEQ_3:25;

now :: thesis: ( ( n1 = 1 & n2 = 1 & x1 = x2 ) or ( n1 = 1 & n2 > 1 & contradiction ) or ( n1 > 1 & n2 = 1 & contradiction ) or ( n1 > 1 & n2 > 1 & x1 = x2 ) )end;

hence
x1 = x2
; :: thesis: verumper cases
( ( n1 = 1 & n2 = 1 ) or ( n1 = 1 & n2 > 1 ) or ( n1 > 1 & n2 = 1 ) or ( n1 > 1 & n2 > 1 ) )
by A60, A58, XXREAL_0:1;

end;

case that A61:
n1 = 1
and

A62: n2 > 1 ; :: thesis: contradiction

A62: n2 > 1 ; :: thesis: contradiction

A63:
n2 - 1 <= (1 + (len (mid (f,((Index (p,f)) + 1),(len f))))) - 1
by A5, A59, XREAL_1:9;

n1 <= len <*p*> by A61, FINSEQ_1:39;

then n1 in dom <*p*> by A61, FINSEQ_3:25;

then A64: g . n1 = <*p*> . n1 by A4, FINSEQ_1:def 7;

n2 - 1 > 0 by A62, XREAL_1:50;

then A65: n2 -' 1 = n2 - 1 by XREAL_0:def 2;

then A66: (len <*p*>) + (n2 -' 1) = 1 + (n2 - 1) by FINSEQ_1:39

.= n2 ;

A67: 1 <= n2 -' 1 by A62, A65, SPPOL_1:1;

then n2 -' 1 in dom (mid (f,((Index (p,f)) + 1),(len f))) by A65, A63, FINSEQ_3:25;

then g . n2 = (mid (f,((Index (p,f)) + 1),(len f))) . (n2 -' 1) by A4, A66, FINSEQ_1:def 7

.= f . (((n2 -' 1) + ((Index (p,f)) + 1)) -' 1) by A7, A17, A21, A65, A63, A67, FINSEQ_6:118

.= f . ((n2 + (Index (p,f))) -' 1) by A65 ;

then A68: f . ((n2 + (Index (p,f))) -' 1) = p by A56, A61, A64, FINSEQ_1:40;

n2 -' 1 <= (len f) - (Index (p,f)) by A47, A48, A59, NAT_D:42;

then n2 - 1 <= (len f) - (Index (p,f)) by A62, XREAL_1:233;

then A69: (n2 - 1) + (Index (p,f)) <= ((len f) - (Index (p,f))) + (Index (p,f)) by XREAL_1:6;

1 + 1 < n2 + (Index (p,f)) by A2, A62, Th8, XREAL_1:8;

then A70: 1 < (n2 + (Index (p,f))) - 1 by XREAL_1:20;

then (n2 + (Index (p,f))) -' 1 = (n2 + (Index (p,f))) - 1 by XREAL_0:def 2;

hence contradiction by A1, A3, A70, A68, A69, Th12; :: thesis: verum

end;n1 <= len <*p*> by A61, FINSEQ_1:39;

then n1 in dom <*p*> by A61, FINSEQ_3:25;

then A64: g . n1 = <*p*> . n1 by A4, FINSEQ_1:def 7;

n2 - 1 > 0 by A62, XREAL_1:50;

then A65: n2 -' 1 = n2 - 1 by XREAL_0:def 2;

then A66: (len <*p*>) + (n2 -' 1) = 1 + (n2 - 1) by FINSEQ_1:39

.= n2 ;

A67: 1 <= n2 -' 1 by A62, A65, SPPOL_1:1;

then n2 -' 1 in dom (mid (f,((Index (p,f)) + 1),(len f))) by A65, A63, FINSEQ_3:25;

then g . n2 = (mid (f,((Index (p,f)) + 1),(len f))) . (n2 -' 1) by A4, A66, FINSEQ_1:def 7

.= f . (((n2 -' 1) + ((Index (p,f)) + 1)) -' 1) by A7, A17, A21, A65, A63, A67, FINSEQ_6:118

.= f . ((n2 + (Index (p,f))) -' 1) by A65 ;

then A68: f . ((n2 + (Index (p,f))) -' 1) = p by A56, A61, A64, FINSEQ_1:40;

n2 -' 1 <= (len f) - (Index (p,f)) by A47, A48, A59, NAT_D:42;

then n2 - 1 <= (len f) - (Index (p,f)) by A62, XREAL_1:233;

then A69: (n2 - 1) + (Index (p,f)) <= ((len f) - (Index (p,f))) + (Index (p,f)) by XREAL_1:6;

1 + 1 < n2 + (Index (p,f)) by A2, A62, Th8, XREAL_1:8;

then A70: 1 < (n2 + (Index (p,f))) - 1 by XREAL_1:20;

then (n2 + (Index (p,f))) -' 1 = (n2 + (Index (p,f))) - 1 by XREAL_0:def 2;

hence contradiction by A1, A3, A70, A68, A69, Th12; :: thesis: verum

case that A71:
n1 > 1
and

A72: n2 = 1 ; :: thesis: contradiction

A72: n2 = 1 ; :: thesis: contradiction

A73:
n1 - 1 <= (1 + (len (mid (f,((Index (p,f)) + 1),(len f))))) - 1
by A5, A57, XREAL_1:9;

n2 <= len <*p*> by A72, FINSEQ_1:39;

then n2 in dom <*p*> by A72, FINSEQ_3:25;

then A74: g . n2 = <*p*> . n2 by A4, FINSEQ_1:def 7;

n1 - 1 > 0 by A71, XREAL_1:50;

then A75: n1 -' 1 = n1 - 1 by XREAL_0:def 2;

then A76: (len <*p*>) + (n1 -' 1) = 1 + (n1 - 1) by FINSEQ_1:39

.= n1 ;

A77: 1 <= n1 -' 1 by A71, A75, SPPOL_1:1;

then n1 -' 1 in dom (mid (f,((Index (p,f)) + 1),(len f))) by A75, A73, FINSEQ_3:25;

then g . n1 = (mid (f,((Index (p,f)) + 1),(len f))) . (n1 -' 1) by A4, A76, FINSEQ_1:def 7

.= f . (((n1 -' 1) + ((Index (p,f)) + 1)) -' 1) by A7, A17, A21, A75, A73, A77, FINSEQ_6:118

.= f . ((n1 + (Index (p,f))) -' 1) by A75 ;

then A78: f . ((n1 + (Index (p,f))) -' 1) = p by A56, A72, A74, FINSEQ_1:40;

n1 -' 1 <= (len f) - (Index (p,f)) by A47, A48, A57, NAT_D:42;

then n1 - 1 <= (len f) - (Index (p,f)) by A71, XREAL_1:233;

then A79: (n1 - 1) + (Index (p,f)) <= ((len f) - (Index (p,f))) + (Index (p,f)) by XREAL_1:6;

1 + 1 < n1 + (Index (p,f)) by A2, A71, Th8, XREAL_1:8;

then A80: 1 < (n1 + (Index (p,f))) - 1 by XREAL_1:20;

then (n1 + (Index (p,f))) -' 1 = (n1 + (Index (p,f))) - 1 by XREAL_0:def 2;

hence contradiction by A1, A3, A80, A78, A79, Th12; :: thesis: verum

end;n2 <= len <*p*> by A72, FINSEQ_1:39;

then n2 in dom <*p*> by A72, FINSEQ_3:25;

then A74: g . n2 = <*p*> . n2 by A4, FINSEQ_1:def 7;

n1 - 1 > 0 by A71, XREAL_1:50;

then A75: n1 -' 1 = n1 - 1 by XREAL_0:def 2;

then A76: (len <*p*>) + (n1 -' 1) = 1 + (n1 - 1) by FINSEQ_1:39

.= n1 ;

A77: 1 <= n1 -' 1 by A71, A75, SPPOL_1:1;

then n1 -' 1 in dom (mid (f,((Index (p,f)) + 1),(len f))) by A75, A73, FINSEQ_3:25;

then g . n1 = (mid (f,((Index (p,f)) + 1),(len f))) . (n1 -' 1) by A4, A76, FINSEQ_1:def 7

.= f . (((n1 -' 1) + ((Index (p,f)) + 1)) -' 1) by A7, A17, A21, A75, A73, A77, FINSEQ_6:118

.= f . ((n1 + (Index (p,f))) -' 1) by A75 ;

then A78: f . ((n1 + (Index (p,f))) -' 1) = p by A56, A72, A74, FINSEQ_1:40;

n1 -' 1 <= (len f) - (Index (p,f)) by A47, A48, A57, NAT_D:42;

then n1 - 1 <= (len f) - (Index (p,f)) by A71, XREAL_1:233;

then A79: (n1 - 1) + (Index (p,f)) <= ((len f) - (Index (p,f))) + (Index (p,f)) by XREAL_1:6;

1 + 1 < n1 + (Index (p,f)) by A2, A71, Th8, XREAL_1:8;

then A80: 1 < (n1 + (Index (p,f))) - 1 by XREAL_1:20;

then (n1 + (Index (p,f))) -' 1 = (n1 + (Index (p,f))) - 1 by XREAL_0:def 2;

hence contradiction by A1, A3, A80, A78, A79, Th12; :: thesis: verum

case that A81:
n1 > 1
and

A82: n2 > 1 ; :: thesis: x1 = x2

A82: n2 > 1 ; :: thesis: x1 = x2

A83:
n2 - 1 > 0
by A82, XREAL_1:50;

then A84: n2 -' 1 = n2 - 1 by XREAL_0:def 2;

then A85: (len <*p*>) + (n2 -' 1) = 1 + (n2 - 1) by FINSEQ_1:39

.= n2 ;

A86: n1 - 1 > 0 by A81, XREAL_1:50;

then A87: n1 -' 1 = n1 - 1 by XREAL_0:def 2;

then A88: 0 + 1 <= n1 -' 1 by A86, NAT_1:13;

then A89: 1 <= (n1 - 1) + (Index (p,f)) by A87, NAT_1:12;

then A90: (n1 + (Index (p,f))) -' 1 = (n1 + (Index (p,f))) - 1 by XREAL_0:def 2;

A91: (len <*p*>) + (n1 -' 1) = 1 + (n1 - 1) by A87, FINSEQ_1:39

.= n1 ;

A92: n1 - 1 <= (1 + (len (mid (f,((Index (p,f)) + 1),(len f))))) - 1 by A5, A57, XREAL_1:9;

then n1 -' 1 in dom (mid (f,((Index (p,f)) + 1),(len f))) by A87, A88, FINSEQ_3:25;

then A93: g . n1 = (mid (f,((Index (p,f)) + 1),(len f))) . (n1 -' 1) by A4, A91, FINSEQ_1:def 7

.= f . (((n1 -' 1) + ((Index (p,f)) + 1)) -' 1) by A7, A17, A21, A87, A88, A92, FINSEQ_6:118

.= f . ((n1 + (Index (p,f))) -' 1) by A87 ;

n1 -' 1 <= (len f) -' (Index (p,f)) by A53, A57, NAT_D:42;

then (n1 -' 1) + (Index (p,f)) <= ((len f) - (Index (p,f))) + (Index (p,f)) by A51, XREAL_1:6;

then A94: (n1 + (Index (p,f))) -' 1 in dom f by A87, A89, A90, FINSEQ_3:25;

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

then A96: 1 <= (n2 -' 1) + (Index (p,f)) by NAT_1:12;

then A97: (n2 + (Index (p,f))) -' 1 = (n2 + (Index (p,f))) - 1 by A84, XREAL_0:def 2;

A98: n2 - 1 <= (1 + (len (mid (f,((Index (p,f)) + 1),(len f))))) - 1 by A5, A59, XREAL_1:9;

then n2 -' 1 in dom (mid (f,((Index (p,f)) + 1),(len f))) by A84, A95, FINSEQ_3:25;

then A99: g . n2 = (mid (f,((Index (p,f)) + 1),(len f))) . (n2 -' 1) by A4, A85, FINSEQ_1:def 7

.= f . (((n2 -' 1) + ((Index (p,f)) + 1)) -' 1) by A7, A17, A21, A84, A95, A98, FINSEQ_6:118

.= f . ((n2 + (Index (p,f))) -' 1) by A84 ;

n2 -' 1 <= (len f) -' (Index (p,f)) by A53, A59, NAT_D:42;

then (n2 -' 1) + (Index (p,f)) <= ((len f) - (Index (p,f))) + (Index (p,f)) by A51, XREAL_1:6;

then (n2 + (Index (p,f))) -' 1 in dom f by A84, A96, A97, FINSEQ_3:25;

then (n1 + (Index (p,f))) -' 1 = (n2 + (Index (p,f))) -' 1 by A1, A56, A99, A93, A94, FUNCT_1:def 4;

hence x1 = x2 by A97, A90; :: thesis: verum

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

then A85: (len <*p*>) + (n2 -' 1) = 1 + (n2 - 1) by FINSEQ_1:39

.= n2 ;

A86: n1 - 1 > 0 by A81, XREAL_1:50;

then A87: n1 -' 1 = n1 - 1 by XREAL_0:def 2;

then A88: 0 + 1 <= n1 -' 1 by A86, NAT_1:13;

then A89: 1 <= (n1 - 1) + (Index (p,f)) by A87, NAT_1:12;

then A90: (n1 + (Index (p,f))) -' 1 = (n1 + (Index (p,f))) - 1 by XREAL_0:def 2;

A91: (len <*p*>) + (n1 -' 1) = 1 + (n1 - 1) by A87, FINSEQ_1:39

.= n1 ;

A92: n1 - 1 <= (1 + (len (mid (f,((Index (p,f)) + 1),(len f))))) - 1 by A5, A57, XREAL_1:9;

then n1 -' 1 in dom (mid (f,((Index (p,f)) + 1),(len f))) by A87, A88, FINSEQ_3:25;

then A93: g . n1 = (mid (f,((Index (p,f)) + 1),(len f))) . (n1 -' 1) by A4, A91, FINSEQ_1:def 7

.= f . (((n1 -' 1) + ((Index (p,f)) + 1)) -' 1) by A7, A17, A21, A87, A88, A92, FINSEQ_6:118

.= f . ((n1 + (Index (p,f))) -' 1) by A87 ;

n1 -' 1 <= (len f) -' (Index (p,f)) by A53, A57, NAT_D:42;

then (n1 -' 1) + (Index (p,f)) <= ((len f) - (Index (p,f))) + (Index (p,f)) by A51, XREAL_1:6;

then A94: (n1 + (Index (p,f))) -' 1 in dom f by A87, A89, A90, FINSEQ_3:25;

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

then A96: 1 <= (n2 -' 1) + (Index (p,f)) by NAT_1:12;

then A97: (n2 + (Index (p,f))) -' 1 = (n2 + (Index (p,f))) - 1 by A84, XREAL_0:def 2;

A98: n2 - 1 <= (1 + (len (mid (f,((Index (p,f)) + 1),(len f))))) - 1 by A5, A59, XREAL_1:9;

then n2 -' 1 in dom (mid (f,((Index (p,f)) + 1),(len f))) by A84, A95, FINSEQ_3:25;

then A99: g . n2 = (mid (f,((Index (p,f)) + 1),(len f))) . (n2 -' 1) by A4, A85, FINSEQ_1:def 7

.= f . (((n2 -' 1) + ((Index (p,f)) + 1)) -' 1) by A7, A17, A21, A84, A95, A98, FINSEQ_6:118

.= f . ((n2 + (Index (p,f))) -' 1) by A84 ;

n2 -' 1 <= (len f) -' (Index (p,f)) by A53, A59, NAT_D:42;

then (n2 -' 1) + (Index (p,f)) <= ((len f) - (Index (p,f))) + (Index (p,f)) by A51, XREAL_1:6;

then (n2 + (Index (p,f))) -' 1 in dom f by A84, A96, A97, FINSEQ_3:25;

then (n1 + (Index (p,f))) -' 1 = (n2 + (Index (p,f))) -' 1 by A1, A56, A99, A93, A94, FUNCT_1:def 4;

hence x1 = x2 by A97, A90; :: thesis: verum

A101: ((len g) - 1) + 1 >= 1 + 1 by A18, A47, XREAL_1:6;

A102: ((len f) -' ((Index (p,f)) + 1)) + 1 = (len f) - (Index (p,f)) by A20;

for j being Nat st 1 <= j & j + 1 <= len g & not (g /. j) `1 = (g /. (j + 1)) `1 holds

(g /. j) `2 = (g /. (j + 1)) `2

proof

then
( g is unfolded & g is s.n.c. & g is special )
by A23, A8, TOPREAL1:def 5, TOPREAL1:def 6, TOPREAL1:def 7;
1 <= Index (p,f)
by A2, Th8;

then A103: 1 < (Index (p,f)) + 1 by NAT_1:13;

let j be Nat; :: thesis: ( 1 <= j & j + 1 <= len g & not (g /. j) `1 = (g /. (j + 1)) `1 implies (g /. j) `2 = (g /. (j + 1)) `2 )

assume that

A104: 1 <= j and

A105: j + 1 <= len g ; :: thesis: ( (g /. j) `1 = (g /. (j + 1)) `1 or (g /. j) `2 = (g /. (j + 1)) `2 )

A106: LSeg (g,j) = LSeg ((g /. j),(g /. (j + 1))) by A104, A105, TOPREAL1:def 3;

(j + 1) - 1 <= (1 + (len (mid (f,((Index (p,f)) + 1),(len f))))) - 1 by A5, A105, XREAL_1:9;

then (j + 1) - 1 <= (len f) - (Index (p,f)) by A7, A17, A21, A102, FINSEQ_6:118;

then A107: j + (Index (p,f)) <= ((len f) - (Index (p,f))) + (Index (p,f)) by XREAL_1:6;

(Index (p,f)) + 1 <= (Index (p,f)) + j by A104, XREAL_1:6;

then 1 < (Index (p,f)) + j by A103, XXREAL_0:2;

then A108: 1 <= ((Index (p,f)) + j) - 1 by SPPOL_1:1;

then A109: ((Index (p,f)) + j) - 1 = ((Index (p,f)) + j) -' 1 by XREAL_0:def 2;

then A110: LSeg (f,(((Index (p,f)) + j) -' 1)) = LSeg ((f /. (((Index (p,f)) + j) -' 1)),(f /. ((((Index (p,f)) + j) -' 1) + 1))) by A108, A107, TOPREAL1:def 3;

A111: ( (f /. (((Index (p,f)) + j) -' 1)) `1 = (f /. ((((Index (p,f)) + j) -' 1) + 1)) `1 or (f /. (((Index (p,f)) + j) -' 1)) `2 = (f /. ((((Index (p,f)) + j) -' 1) + 1)) `2 ) by A1, A108, A109, A107, TOPREAL1:def 5;

LSeg (g,j) c= LSeg (f,(((Index (p,f)) + j) -' 1)) by A2, A4, A104, A105, Th16;

hence ( (g /. j) `1 = (g /. (j + 1)) `1 or (g /. j) `2 = (g /. (j + 1)) `2 ) by A106, A110, A111, Th3; :: thesis: verum

end;then A103: 1 < (Index (p,f)) + 1 by NAT_1:13;

let j be Nat; :: thesis: ( 1 <= j & j + 1 <= len g & not (g /. j) `1 = (g /. (j + 1)) `1 implies (g /. j) `2 = (g /. (j + 1)) `2 )

assume that

A104: 1 <= j and

A105: j + 1 <= len g ; :: thesis: ( (g /. j) `1 = (g /. (j + 1)) `1 or (g /. j) `2 = (g /. (j + 1)) `2 )

A106: LSeg (g,j) = LSeg ((g /. j),(g /. (j + 1))) by A104, A105, TOPREAL1:def 3;

(j + 1) - 1 <= (1 + (len (mid (f,((Index (p,f)) + 1),(len f))))) - 1 by A5, A105, XREAL_1:9;

then (j + 1) - 1 <= (len f) - (Index (p,f)) by A7, A17, A21, A102, FINSEQ_6:118;

then A107: j + (Index (p,f)) <= ((len f) - (Index (p,f))) + (Index (p,f)) by XREAL_1:6;

(Index (p,f)) + 1 <= (Index (p,f)) + j by A104, XREAL_1:6;

then 1 < (Index (p,f)) + j by A103, XXREAL_0:2;

then A108: 1 <= ((Index (p,f)) + j) - 1 by SPPOL_1:1;

then A109: ((Index (p,f)) + j) - 1 = ((Index (p,f)) + j) -' 1 by XREAL_0:def 2;

then A110: LSeg (f,(((Index (p,f)) + j) -' 1)) = LSeg ((f /. (((Index (p,f)) + j) -' 1)),(f /. ((((Index (p,f)) + j) -' 1) + 1))) by A108, A107, TOPREAL1:def 3;

A111: ( (f /. (((Index (p,f)) + j) -' 1)) `1 = (f /. ((((Index (p,f)) + j) -' 1) + 1)) `1 or (f /. (((Index (p,f)) + j) -' 1)) `2 = (f /. ((((Index (p,f)) + j) -' 1) + 1)) `2 ) by A1, A108, A109, A107, TOPREAL1:def 5;

LSeg (g,j) c= LSeg (f,(((Index (p,f)) + j) -' 1)) by A2, A4, A104, A105, Th16;

hence ( (g /. j) `1 = (g /. (j + 1)) `1 or (g /. j) `2 = (g /. (j + 1)) `2 ) by A106, A110, A111, Th3; :: thesis: verum

then A112: g is being_S-Seq by A101, A100, TOPREAL1:def 8;

A113: ((len f) -' (Index (p,f))) + ((Index (p,f)) + 1) = ((len f) - (Index (p,f))) + ((Index (p,f)) + 1) by A50, XREAL_0:def 2

.= (len f) + 1 ;

1 + ((len g) -' 1) = 1 + ((len g) - 1) by A46, XREAL_0:def 2

.= len g ;

then g . (len g) = g . ((len <*p*>) + ((len g) -' 1)) by FINSEQ_1:39

.= (mid (f,((Index (p,f)) + 1),(len f))) . ((len g) -' 1) by A4, A49, FINSEQ_1:def 7 ;

then g . (len g) = f . (len f) by A47, A48, A52, A113, NAT_D:34;

then A114: g . (len g) = f /. (len f) by A7, FINSEQ_4:15;

g . 1 = p by A4, FINSEQ_1:41;

hence g is_S-Seq_joining p,f /. (len f) by A112, A114; :: thesis: verum