let n be Nat; :: thesis: for f being FinSequence of REAL st n in dom f holds
(f | n) . 1 = f . 1
let f be FinSequence of REAL ; :: thesis: ( n in dom f implies (f | n) . 1 = f . 1 )
assume A1: n in dom f ; :: thesis: (f | n) . 1 = f . 1
then n >= 1 by FINSEQ_3:24, NAT_1:14;
hence (f | n) . 1 = f . 1 by A1, Th7; :: thesis: verum