let m, n be Nat; :: thesis: for f being FinSequence of REAL st n in dom f & 1 <= m & m <= n holds

f . m = (f | n) . m

let f be FinSequence of REAL ; :: thesis: ( n in dom f & 1 <= m & m <= n implies f . m = (f | n) . m )

assume A1: ( n in dom f & 1 <= m & m <= n ) ; :: thesis: f . m = (f | n) . m

then m in Seg n ;

hence f . m = (f | n) . m by A1, RFINSEQ:6; :: thesis: verum

f . m = (f | n) . m

let f be FinSequence of REAL ; :: thesis: ( n in dom f & 1 <= m & m <= n implies f . m = (f | n) . m )

assume A1: ( n in dom f & 1 <= m & m <= n ) ; :: thesis: f . m = (f | n) . m

then m in Seg n ;

hence f . m = (f | n) . m by A1, RFINSEQ:6; :: thesis: verum