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
set c = (1 + 1),(len g) -cut g;
set k = (len f) -' 1;
reconsider g9 = g as unfolded FinSequence of (TOP-REAL 2) by A2;
A5: (1 + 1),(len g) -cut g = g9 /^ 1 by Th13;
A6: f ^' g = f ^ ((1 + 1),(len g) -cut g) by GRAPH_2:def 2;

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 f is empty ; :: thesis: f ^' g is unfolded

hence f ^' g is unfolded by A6, A5, FINSEQ_1:47; :: thesis: verum

end;

suppose len g = 0 ; :: thesis: f ^' g is unfolded

then g = {} ;
then (1 + 1),(len g) -cut g = <*> the carrier of (TOP-REAL 2) by A5, FINSEQ_6:86;
hence f ^' g is unfolded by A1, A6, FINSEQ_1:47; :: thesis: verum

end;

suppose len g = 1 ; :: thesis: f ^' g is unfolded

then (1 + 1),(len g) -cut g = {} by A5, REVROT_1:2;
hence f ^' g is unfolded by A1, A6, FINSEQ_1:47; :: thesis: verum

end;

suppose that A7: not f is empty and
A8: len g = 1 + 1 ; :: thesis: f ^' g is unfolded

A9: ((len f) -' 1) + 1 = len f by A7, NAT_1:14, XREAL_1:237;
g | (len g) = g by FINSEQ_1:79;
then g = <*(g /. 1),(g /. 2)*> by A8, FINSEQ_5:84;
then A10: f ^' g = f ^ <*(g /. 2)*> by A6, A5, 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 A5, 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

A15: 1 <= len g by A14, XXREAL_0:2;
then A16: LSeg (g /^ 1),1 = LSeg g,(1 + 1) by SPPOL_2:4;
1 + 1 <= len g by A14;
then 1 <= (len g) - 1 by XREAL_1:21;
then 1 <= len (g /^ 1) by A15, RFINSEQ:def 2;
then A17: 1 in dom (g /^ 1) by FINSEQ_3:27;
then A18: ((1 + 1),(len g) -cut g) /. 1 = (g /^ 1) . 1 by A5, PARTFUN1:def 8
.= g . (1 + 1) by A15, A17, RFINSEQ:def 2
.= g /. (1 + 1) by A14, FINSEQ_4:24 ;
then A19: LSeg g,1 = LSeg (f /. (len f)),(((1 + 1),(len g) -cut g) /. 1) by A3, A14, TOPREAL1:def 5;
A20: ((len f) -' 1) + 1 = len f by A13, NAT_1:14, XREAL_1:237;
1 + 2 <= len g by A14, NAT_1:13;
then (LSeg g,1) /\ (LSeg ((1 + 1),(len g) -cut g),1) = {(((1 + 1),(len g) -cut g) /. 1)} by A5, A18, A16, TOPREAL1:def 8;
hence f ^' g is unfolded by A1, A4, A6, A5, A20, A19, SPPOL_2:32; :: thesis: verum

end;

end;