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