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 A2: ( 1 in dom p & len p in dom p ) by FINSEQ_5:6;
A3: (len p) + 1 = len q by Def10;
p . 1 in Funcs (q . 1),(q . (1 + 1)) by A2, Def10;
then consider f being Function such that
A4: ( p . 1 = f & dom f = q . 1 & rng f c= q . 2 ) by FUNCT_2:def 2;
thus firstdom p = q . 1 by A1, A4, Def6; :: thesis: lastrng p c= q . (len q)
p . (len p) in Funcs (q . (len p)),(q . ((len p) + 1)) by A2, Def10;
then consider g being Function such that
A5: ( p . (len p) = g & dom g = q . (len p) & rng g c= q . ((len p) + 1) ) by FUNCT_2:def 2;
thus lastrng p c= q . (len q) by A1, A3, A5, Def7; :: thesis: verum