let D be set ; :: thesis: for f being FinSequence
for g being XFinSequence of D holds (f ^ g) /^ (len f) = XFS2FS g
let f be FinSequence; :: thesis: for g being XFinSequence of D holds (f ^ g) /^ (len f) = XFS2FS g
let g be XFinSequence of D; :: thesis: (f ^ g) /^ (len f) = XFS2FS g
(len f) + 0 <= (len f) + (len g) by XREAL_1:6;
then A0: len f <= len (f ^ g) by XL1;
A1: len g = ((len f) + (len g)) - (len f)
.= (len (f ^ g)) - (len f) by XL1
.= len ((f ^ g) /^ (len f)) by A0, RFINSEQ:def 1 ;
len (XFS2FS g) = len g by AFINSQ_1:def 9;
then A3: dom (XFS2FS g) = Seg (len g) by FINSEQ_1:def 3
.= dom ((f ^ g) /^ (len f)) by A1, FINSEQ_1:def 3 ;
for i being Nat st i in dom ((f ^ g) /^ (len f)) holds
((f ^ g) /^ (len f)) . i = (XFS2FS g) . i

proof

let i be Nat; :: thesis: ( i in dom ((f ^ g) /^ (len f)) implies ((f ^ g) /^ (len f)) . i = (XFS2FS g) . i )
assume B1: i in dom ((f ^ g) /^ (len f)) ; :: thesis: ((f ^ g) /^ (len f)) . i = (XFS2FS g) . i
then i in Seg (len g) by A1, FINSEQ_1:def 3;
then B3: ( 1 <= i & i <= len g ) by FINSEQ_1:1;
then reconsider j = i - 1 as Nat ;
j + 1 in Seg (len g) by B1, A1, FINSEQ_1:def 3;
then B4: j in Segm (len g) by NEWTON02:106;
(XFS2FS g) . (j + 1) = g . ((j + 1) -' 1) by B3, AFINSQ_1:def 9
.= (f ^ g) . (((len f) + j) + 1) by B4, Def2
.= (f ^ g) . ((len f) + i)
.= ((f ^ g) /^ (len f)) . i by A0, B1, RFINSEQ:def 1 ;
hence ((f ^ g) /^ (len f)) . i = (XFS2FS g) . i ; :: thesis: verum

end;

hence (f ^ g) /^ (len f) = XFS2FS g by A3; :: thesis: verum