let f be FinSequence; :: thesis: for y being object st y in rng f holds
ex n being Nat st
( 1 <= n & n <= len f & y = f . n )
let y be object ; :: thesis: ( y in rng f implies ex n being Nat st
( 1 <= n & n <= len f & y = f . n ) )
assume y in rng f ; :: thesis: ex n being Nat st
( 1 <= n & n <= len f & y = f . n )
then consider n being object such that
A1: n in dom f and
A2: f . n = y by FUNCT_1:def 3;
reconsider n = n as Nat by A1;
take n ; :: thesis: ( 1 <= n & n <= len f & y = f . n )
thus ( 1 <= n & n <= len f & y = f . n ) by A1, A2, FINSEQ_3:25; :: thesis: verum