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