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