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