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

(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