let n be Nat; :: thesis: for f being FinSequence of REAL
for D being set st f is FinSequence of D holds
( f | n is FinSequence of D & f /^ n is FinSequence of D )
let f be FinSequence of REAL ; :: thesis: for D being set st f is FinSequence of D holds
( f | n is FinSequence of D & f /^ n is FinSequence of D )
let D be set ; :: thesis: ( f is FinSequence of D implies ( f | n is FinSequence of D & f /^ n is FinSequence of D ) )
assume A1: f is FinSequence of D ; :: thesis: ( f | n is FinSequence of D & f /^ n is FinSequence of D )
(f | n) ^ (f /^ n) = f by RFINSEQ:8;
hence ( f | n is FinSequence of D & f /^ n is FinSequence of D ) by A1, FINSEQ_1:36; :: thesis: verum