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

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