let D be set ; :: thesis: for f being XFinSequence
for g being FinSequence of D holds (f ^ g) /^ (len f) = FS2XFS g
let f be XFinSequence; :: thesis: for g being FinSequence of D holds (f ^ g) /^ (len f) = FS2XFS g
let g be FinSequence of D; :: thesis: (f ^ g) /^ (len f) = FS2XFS g
len (f ^ g) = (len f) + (len g) by Def1;
then A1: len ((f ^ g) /^ (len f)) = ((len f) + (len g)) -' (len f) by AFINSQ_2:def 2
.= len g ;
for i being Nat st i in dom ((f ^ g) /^ (len f)) holds
((f ^ g) /^ (len f)) . i = (FS2XFS g) . i

proof

let i be Nat; :: thesis: ( i in dom ((f ^ g) /^ (len f)) implies ((f ^ g) /^ (len f)) . i = (FS2XFS g) . i )
assume B1: i in dom ((f ^ g) /^ (len f)) ; :: thesis: ((f ^ g) /^ (len f)) . i = (FS2XFS g) . i
then B2: i in Segm (len g) by A1;
then i + 1 in Seg (len g) by NEWTON02:106;
then B4: i + 1 in dom g by FINSEQ_1:def 3;
(FS2XFS g) . i = g . (i + 1) by B2, NAT_1:44, AFINSQ_1:def 8
.= (f ^ g) . (((len f) + (i + 1)) - 1) by B4, Def1
.= (f ^ g) . ((len f) + i)
.= ((f ^ g) /^ (len f)) . i by B1, AFINSQ_2:def 2 ;
hence ((f ^ g) /^ (len f)) . i = (FS2XFS g) . i ; :: thesis: verum

end;

hence (f ^ g) /^ (len f) = FS2XFS g by A1, AFINSQ_1:def 8; :: thesis: verum