let f, g be FinSequence of (TOP-REAL 2); :: thesis: ( f is unfolded & g is unfolded & f /. (len f) = g /. 1 & (LSeg f,((len f) -' 1)) /\ (LSeg g,1) = {(f /. (len f))} implies f ^' g is unfolded )
assume that
A1:
f is unfolded
and
A2:
g is unfolded
and
A3:
f /. (len f) = g /. 1
and
A4:
(LSeg f,((len f) -' 1)) /\ (LSeg g,1) = {(f /. (len f))}
; :: thesis: f ^' g is unfolded
A5:
f ^' g = f ^ ((1 + 1),(len g) -cut g)
by GRAPH_2:def 2;
reconsider g' = g as unfolded FinSequence of (TOP-REAL 2) by A2;
set c = (1 + 1),(len g) -cut g;
set k = (len f) -' 1;
A6:
(1 + 1),(len g) -cut g = g' /^ 1
by Th13;
per cases
( f is empty or len g = 0 or len g = 1 or ( not f is empty & len g = 1 + 1 ) or ( not f is empty & 2 < len g ) )
by NAT_1:27;
suppose that A7:
not
f is
empty
and A8:
len g = 1
+ 1
;
:: thesis: f ^' g is unfolded
len f <> 0
by A7;
then A9:
((len f) -' 1) + 1
= len f
by NAT_1:14, XREAL_1:237;
g | (len g) = g
by FINSEQ_1:79;
then
g = <*(g /. 1),(g /. 2)*>
by A8, JORDAN8:1;
then A10:
f ^' g = f ^ <*(g /. 2)*>
by A5, A6, FINSEQ_6:50;
1
<= (len g) - 1
by A8;
then
1
<= len (g /^ 1)
by A8, RFINSEQ:def 2;
then A11:
1
in dom (g /^ 1)
by FINSEQ_3:27;
then A12:
((1 + 1),(len g) -cut g) /. 1 =
(g /^ 1) . 1
by A6, PARTFUN1:def 8
.=
g . (1 + 1)
by A8, A11, RFINSEQ:def 2
.=
g /. (1 + 1)
by A8, FINSEQ_4:24
;
then
LSeg g,1
= LSeg (f /. (len f)),
(((1 + 1),(len g) -cut g) /. 1)
by A3, A8, TOPREAL1:def 5;
hence
f ^' g is
unfolded
by A1, A4, A9, A10, A12, SPPOL_2:31;
:: thesis: verum end; suppose that A13:
not
f is
empty
and A14:
2
< len g
;
:: thesis: f ^' g is unfolded
len f <> 0
by A13;
then A15:
((len f) -' 1) + 1
= len f
by NAT_1:14, XREAL_1:237;
A16:
1
+ 2
<= len g
by A14, NAT_1:13;
A17:
1
+ 1
<= len g
by A14;
A18:
1
<= len g
by A14, XXREAL_0:2;
1
<= (len g) - 1
by A17, XREAL_1:21;
then
1
<= len (g /^ 1)
by A18, RFINSEQ:def 2;
then A19:
1
in dom (g /^ 1)
by FINSEQ_3:27;
then A20:
((1 + 1),(len g) -cut g) /. 1 =
(g /^ 1) . 1
by A6, PARTFUN1:def 8
.=
g . (1 + 1)
by A18, A19, RFINSEQ:def 2
.=
g /. (1 + 1)
by A14, FINSEQ_4:24
;
then A21:
LSeg g,1
= LSeg (f /. (len f)),
(((1 + 1),(len g) -cut g) /. 1)
by A3, A14, TOPREAL1:def 5;
LSeg (g /^ 1),1
= LSeg g,
(1 + 1)
by A18, SPPOL_2:4;
then
(LSeg g,1) /\ (LSeg ((1 + 1),(len g) -cut g),1) = {(((1 + 1),(len g) -cut g) /. 1)}
by A6, A16, A20, TOPREAL1:def 8;
hence
f ^' g is
unfolded
by A1, A4, A5, A6, A15, A21, SPPOL_2:32;
:: thesis: verum end;