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

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