let D be set ; :: thesis: for p being FinSequence of D
for n being Nat holds
( (FS2XFS p) | n = FS2XFS (p | n) & (FS2XFS p) /^ n = FS2XFS (p /^ n) )
let p be FinSequence of D; :: thesis: for n being Nat holds
( (FS2XFS p) | n = FS2XFS (p | n) & (FS2XFS p) /^ n = FS2XFS (p /^ n) )
let n be Nat; :: thesis: ( (FS2XFS p) | n = FS2XFS (p | n) & (FS2XFS p) /^ n = FS2XFS (p /^ n) )
thus (FS2XFS p) | n = FS2XFS (XFS2FS ((FS2XFS p) | n))
.= FS2XFS ((XFS2FS (FS2XFS p)) | n) by Th17
.= FS2XFS (p | n) ; :: thesis: (FS2XFS p) /^ n = FS2XFS (p /^ n)
thus (FS2XFS p) /^ n = FS2XFS (XFS2FS ((FS2XFS p) /^ n))
.= FS2XFS ((XFS2FS (FS2XFS p)) /^ n) by Th17
.= FS2XFS (p /^ n) ; :: thesis: verum