let D be set ; :: thesis: for f being XFinSequence of D
for g being FinSequence of D holds XFS2FS (f ^ g) = (XFS2FS f) ^ g
let f be XFinSequence of D; :: thesis: for g being FinSequence of D holds XFS2FS (f ^ g) = (XFS2FS f) ^ g
let g be FinSequence of D; :: thesis: XFS2FS (f ^ g) = (XFS2FS f) ^ g
(XFS2FS f) ^ (XFS2FS (FS2XFS g)) = XFS2FS (f ^ (FS2XFS g)) by SXX;
hence XFS2FS (f ^ g) = (XFS2FS f) ^ g by XFX; :: thesis: verum