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 FINSEQ_6:def 5;
( len g <= 2 implies not not len g = 0 & ... & not len g = 2 ) ;

per cases then ( 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 ) ) ;

suppose f is empty ; :: thesis: f ^' g is unfolded

hence f ^' g is unfolded by A6, A5, FINSEQ_1:34; :: 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:80;
hence f ^' g is unfolded by A1, A6, FINSEQ_1:34; :: thesis: verum

end;

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

then ((1 + 1),(len g)) -cut g = {} by A5, FINSEQ_6:167;
hence f ^' g is unfolded by A1, A6, FINSEQ_1:34; :: 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:235;
g | (len g) = g by FINSEQ_1:58;
then g = <*(g /. 1),(g /. 2)*> by A8, FINSEQ_5:81;
then A10: f ^' g = f ^ <*(g /. 2)*> by A6, A5, FINSEQ_6:46;
1 <= (len g) - 1 by A8;
then 1 <= len (g /^ 1) by A8, RFINSEQ:def 1;
then A11: 1 in dom (g /^ 1) by FINSEQ_3:25;
then A12: (((1 + 1),(len g)) -cut g) /. 1 = (g /^ 1) . 1 by A5, PARTFUN1:def 6
.= g . (1 + 1) by A8, A11, RFINSEQ:def 1
.= g /. (1 + 1) by A8, FINSEQ_4:15 ;
then LSeg (g,1) = LSeg ((f /. (len f)),((((1 + 1),(len g)) -cut g) /. 1)) by A3, A8, TOPREAL1:def 3;
hence f ^' g is unfolded by A1, A4, A9, A10, A12, SPPOL_2:30; :: 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:19;
then 1 <= len (g /^ 1) by A15, RFINSEQ:def 1;
then A17: 1 in dom (g /^ 1) by FINSEQ_3:25;
then A18: (((1 + 1),(len g)) -cut g) /. 1 = (g /^ 1) . 1 by A5, PARTFUN1:def 6
.= g . (1 + 1) by A15, A17, RFINSEQ:def 1
.= g /. (1 + 1) by A14, FINSEQ_4:15 ;
then A19: LSeg (g,1) = LSeg ((f /. (len f)),((((1 + 1),(len g)) -cut g) /. 1)) by A3, A14, TOPREAL1:def 3;
A20: ((len f) -' 1) + 1 = len f by A13, NAT_1:14, XREAL_1:235;
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 6;
hence f ^' g is unfolded by A1, A4, A6, A5, A20, A19, SPPOL_2:31; :: thesis: verum

end;

end;