let f, g be FinSequence of (TOP-REAL 2); :: thesis: ( not f is empty & not g is empty implies LSeg ((f ^ g),(len f)) = LSeg ((f /. (len f)),(g /. 1)) )
assume that
A1: not f is empty and
A2: not g is empty ; :: thesis: LSeg ((f ^ g),(len f)) = LSeg ((f /. (len f)),(g /. 1))
A3: 1 in dom g by A2, FINSEQ_5:6;
then 1 <= len g by FINSEQ_3:25;
then (len f) + 1 <= (len f) + (len g) by XREAL_1:6;
then A4: (len f) + 1 <= len (f ^ g) by FINSEQ_1:22;
A5: len f in dom f by A1, FINSEQ_5:6;
then 1 <= len f by FINSEQ_3:25;
hence LSeg ((f ^ g),(len f)) = LSeg (((f ^ g) /. (len f)),((f ^ g) /. ((len f) + 1))) by A4, TOPREAL1:def 3
.= LSeg ((f /. (len f)),((f ^ g) /. ((len f) + 1))) by A5, FINSEQ_4:68
.= LSeg ((f /. (len f)),(g /. 1)) by A3, FINSEQ_4:69 ;
:: thesis: verum