let f, g be FinSequence of (TOP-REAL 2); :: thesis: for k being Element of NAT st f is unfolded & g is unfolded & k + 1 = len f & (LSeg f,k) /\ (LSeg (f /. (len f)),(g /. 1)) = {(f /. (len f))} & (LSeg (f /. (len f)),(g /. 1)) /\ (LSeg g,1) = {(g /. 1)} holds
f ^ g is unfolded
let k be Element of NAT ; :: thesis: ( f is unfolded & g is unfolded & k + 1 = len f & (LSeg f,k) /\ (LSeg (f /. (len f)),(g /. 1)) = {(f /. (len f))} & (LSeg (f /. (len f)),(g /. 1)) /\ (LSeg g,1) = {(g /. 1)} implies f ^ g is unfolded )
assume that
A1: f is unfolded and
A2: g is unfolded and
A3: ( k + 1 = len f & (LSeg f,k) /\ (LSeg (f /. (len f)),(g /. 1)) = {(f /. (len f))} ) and
A4: (LSeg (f /. (len f)),(g /. 1)) /\ (LSeg g,1) = {(g /. 1)} ; :: thesis: f ^ g is unfolded
let i be Nat; :: according to TOPREAL1:def 8 :: thesis: ( not 1 <= i or not i + 2 <= len (f ^ g) or (LSeg (f ^ g),i) /\ (LSeg (f ^ g),(i + 1)) = {((f ^ g) /. (i + 1))} )
assume that
A5: 1 <= i and
A6: i + 2 <= len (f ^ g) ; :: thesis: (LSeg (f ^ g),i) /\ (LSeg (f ^ g),(i + 1)) = {((f ^ g) /. (i + 1))}
A7: len (f ^ g) = (len f) + (len g) by FINSEQ_1:35;

per cases ( i + 2 <= len f or i + 2 > len f ) ;

suppose A8: i + 2 <= len f ; :: thesis: (LSeg (f ^ g),i) /\ (LSeg (f ^ g),(i + 1)) = {((f ^ g) /. (i + 1))}

then A9: i + 1 in dom f by A5, GOBOARD2:4;
A10: i + (1 + 1) = (i + 1) + 1 ;
i + 1 <= (i + 1) + 1 by NAT_1:11;
hence (LSeg (f ^ g),i) /\ (LSeg (f ^ g),(i + 1)) = (LSeg f,i) /\ (LSeg (f ^ g),(i + 1)) by A8, Th6, XXREAL_0:2
.= (LSeg f,i) /\ (LSeg f,(i + 1)) by A8, A10, Th6
.= {(f /. (i + 1))} by A1, A5, A8, TOPREAL1:def 8
.= {((f ^ g) /. (i + 1))} by A9, FINSEQ_4:83 ;
:: thesis: verum

end;

suppose A11: i + 2 > len f ; :: thesis: (LSeg (f ^ g),i) /\ (LSeg (f ^ g),(i + 1)) = {((f ^ g) /. (i + 1))}

A12: i + (1 + 1) = (i + 1) + 1 ;

now

per cases ( i <= len f or i > len f ) ;

suppose A13: i <= len f ; :: thesis: (LSeg (f ^ g),i) /\ (LSeg (f ^ g),(i + 1)) = {((f ^ g) /. (i + 1))}

then A14: not f is empty by A5;
len g <> 0 by A6, A7, A11;
then 1 <= len g by NAT_1:14;
then A15: 1 in dom g by FINSEQ_3:27;

now

per cases ( i = len f or i <> len f ) ;

suppose A16: i = len f ; :: thesis: (LSeg (f ^ g),i) /\ (LSeg (f ^ g),(i + 1)) = {((f ^ g) /. (i + 1))}

then A17: LSeg (f ^ g),i = LSeg (f /. (len f)),(g /. 1) by A14, A15, Th8, RELAT_1:60;
LSeg (f ^ g),(i + 1) = LSeg g,1 by A16, Th7;
hence (LSeg (f ^ g),i) /\ (LSeg (f ^ g),(i + 1)) = {((f ^ g) /. (i + 1))} by A4, A15, A16, A17, FINSEQ_4:84; :: thesis: verum

end;

suppose i <> len f ; :: thesis: (LSeg (f ^ g),i) /\ (LSeg (f ^ g),(i + 1)) = {((f ^ g) /. (i + 1))}

then i < len f by A13, XXREAL_0:1;
then A18: i + 1 <= len f by NAT_1:13;
len f <= i + 1 by A11, A12, NAT_1:13;
then A19: i + 1 = len f by A18, XXREAL_0:1;
then A20: LSeg (f ^ g),i = LSeg f,k by A3, Th6;
A21: LSeg (f ^ g),(i + 1) = LSeg (f /. (len f)),(g /. 1) by A14, A15, A19, Th8, RELAT_1:60;
len f in dom f by A14, FINSEQ_5:6;
hence (LSeg (f ^ g),i) /\ (LSeg (f ^ g),(i + 1)) = {((f ^ g) /. (i + 1))} by A3, A19, A20, A21, FINSEQ_4:83; :: thesis: verum

end;

end;

end;

hence (LSeg (f ^ g),i) /\ (LSeg (f ^ g),(i + 1)) = {((f ^ g) /. (i + 1))} ; :: thesis: verum

end;

suppose A22: i > len f ; :: thesis: (LSeg (f ^ g),i) /\ (LSeg (f ^ g),(i + 1)) = {((f ^ g) /. (i + 1))}

then reconsider j = i - (len f) as Element of NAT by INT_1:18;
A23: (len f) + j = i ;
A24: (len f) + (j + 1) = i + 1 ;
(len f) + 1 <= i by A22, NAT_1:13;
then A25: 1 <= j by XREAL_1:21;
A26: (i + 2) - (len f) <= len g by A6, A7, XREAL_1:22;
then A27: j + (1 + 1) <= len g ;
j + 1 <= (j + 1) + 1 by NAT_1:11;
then j + 1 <= len g by A26, XXREAL_0:2;
then A28: j + 1 in dom g by A25, GOBOARD2:3;
thus (LSeg (f ^ g),i) /\ (LSeg (f ^ g),(i + 1)) = (LSeg g,j) /\ (LSeg (f ^ g),(i + 1)) by A23, A25, Th7
.= (LSeg g,j) /\ (LSeg g,(j + 1)) by A24, Th7, NAT_1:11
.= {(g /. (j + 1))} by A2, A25, A27, TOPREAL1:def 8
.= {((f ^ g) /. (i + 1))} by A24, A28, FINSEQ_4:84 ; :: thesis: verum

end;

end;

end;

hence (LSeg (f ^ g),i) /\ (LSeg (f ^ g),(i + 1)) = {((f ^ g) /. (i + 1))} ; :: thesis: verum

end;

end;