let f, g be FinSequence of (TOP-REAL 2); :: thesis: for k being 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 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 and
A4: (LSeg (f,k)) /\ (LSeg ((f /. (len f)),(g /. 1))) = {(f /. (len f))} and
A5: (LSeg ((f /. (len f)),(g /. 1))) /\ (LSeg (g,1)) = {(g /. 1)} ; :: thesis: f ^ g is unfolded
let i be Nat; :: according to TOPREAL1:def 6 :: 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
A6: 1 <= i and
A7: i + 2 <= len (f ^ g) ; :: thesis: (LSeg ((f ^ g),i)) /\ (LSeg ((f ^ g),(i + 1))) = {((f ^ g) /. (i + 1))}
A8: len (f ^ g) = (len f) + (len g) by FINSEQ_1:22;

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

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

then A10: i + 1 in dom f by A6, SEQ_4:135;
A11: 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 A9, Th6, XXREAL_0:2
.= (LSeg (f,i)) /\ (LSeg (f,(i + 1))) by A9, A11, Th6
.= {(f /. (i + 1))} by A1, A6, A9
.= {((f ^ g) /. (i + 1))} by A10, FINSEQ_4:68 ;
:: thesis: verum

end;

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

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

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

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

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

len g <> 0 by A7, A8, A12;
then 1 <= len g by NAT_1:14;
then A15: 1 in dom g by FINSEQ_3:25;
A16: not f is empty by A6, A14;

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

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

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

then A18: LSeg ((f ^ g),(i + 1)) = LSeg (g,1) by Th7;
LSeg ((f ^ g),i) = LSeg ((f /. (len f)),(g /. 1)) by A16, A15, A17, Th8, RELAT_1:38;
hence (LSeg ((f ^ g),i)) /\ (LSeg ((f ^ g),(i + 1))) = {((f ^ g) /. (i + 1))} by A5, A15, A17, A18, FINSEQ_4:69; :: 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 A14, XXREAL_0:1;
then A19: i + 1 <= len f by NAT_1:13;
len f <= i + 1 by A12, A13, NAT_1:13;
then A20: i + 1 = len f by A19, XXREAL_0:1;
then A21: LSeg ((f ^ g),i) = LSeg (f,k) by A3, Th6;
A22: len f in dom f by A16, FINSEQ_5:6;
LSeg ((f ^ g),(i + 1)) = LSeg ((f /. (len f)),(g /. 1)) by A16, A15, A20, Th8, RELAT_1:38;
hence (LSeg ((f ^ g),i)) /\ (LSeg ((f ^ g),(i + 1))) = {((f ^ g) /. (i + 1))} by A4, A20, A21, A22, FINSEQ_4:68; :: thesis: verum

end;

end;

end;

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

end;

suppose A23: 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:5;
(len f) + 1 <= i by A23, NAT_1:13;
then A24: 1 <= j by XREAL_1:19;
A25: (i + 2) - (len f) <= len g by A7, A8, XREAL_1:20;
then A26: j + (1 + 1) <= len g ;
j + 1 <= (j + 1) + 1 by NAT_1:11;
then j + 1 <= len g by A25, XXREAL_0:2;
then A27: j + 1 in dom g by A24, SEQ_4:134;
A28: (len f) + (j + 1) = i + 1 ;
(len f) + j = i ;
hence (LSeg ((f ^ g),i)) /\ (LSeg ((f ^ g),(i + 1))) = (LSeg (g,j)) /\ (LSeg ((f ^ g),(i + 1))) by A24, Th7
.= (LSeg (g,j)) /\ (LSeg (g,(j + 1))) by A28, Th7, NAT_1:11
.= {(g /. (j + 1))} by A2, A24, A26
.= {((f ^ g) /. (i + 1))} by A28, A27, FINSEQ_4:69 ;
:: thesis: verum

end;

end;

end;

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

end;

end;