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:27;
then (len f) + 1 <= (len f) + (len g) by XREAL_1:8;
then A4: (len f) + 1 <= len (f ^ g) by FINSEQ_1:35;
A5: len f in dom f by A1, FINSEQ_5:6;
then 1 <= len f by FINSEQ_3:27;
hence LSeg ((f ^ g),(len f)) = LSeg (((f ^ g) /. (len f)),((f ^ g) /. ((len f) + 1))) by A4, TOPREAL1:def 5
.= LSeg ((f /. (len f)),((f ^ g) /. ((len f) + 1))) by A5, FINSEQ_4:83
.= LSeg ((f /. (len f)),(g /. 1)) by A3, FINSEQ_4:84 ;
:: thesis: verum