let q be non empty non-empty FinSequence; :: thesis: for p being FuncSequence of q st p <> {} holds
( firstdom p = q . 1 & lastrng p c= q . (len q) )
let p be FuncSequence of q; :: thesis: ( p <> {} implies ( firstdom p = q . 1 & lastrng p c= q . (len q) ) )
assume A1: p <> {} ; :: thesis: ( firstdom p = q . 1 & lastrng p c= q . (len q) )
then 1 in dom p by FINSEQ_5:6;
then p . 1 in Funcs ((q . 1),(q . (1 + 1))) by Def9;
then ex f being Function st
( p . 1 = f & dom f = q . 1 & rng f c= q . 2 ) by FUNCT_2:def 2;
hence firstdom p = q . 1 by A1, Def5; :: thesis: lastrng p c= q . (len q)
len p in dom p by A1, FINSEQ_5:6;
then p . (len p) in Funcs ((q . (len p)),(q . ((len p) + 1))) by Def9;
then A2: ex g being Function st
( p . (len p) = g & dom g = q . (len p) & rng g c= q . ((len p) + 1) ) by FUNCT_2:def 2;
(len p) + 1 = len q by Def9;
hence lastrng p c= q . (len q) by A1, A2, Def6; :: thesis: verum