let D be set ; :: thesis: for p being XFinSequence of D holds rng p = rng (XFS2FS p)
let p be XFinSequence of D; :: thesis: rng p = rng (XFS2FS p)
thus rng p = rng (FS2XFS (XFS2FS p))
.= rng (XFS2FS p) by Th15 ; :: thesis: verum