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