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