let q be non empty non-empty FinSequence; :: thesis: for p being FuncSequence of q holds
( dom (compose (p,(q . 1))) = q . 1 & rng (compose (p,(q . 1))) c= q . (len q) )
let p be FuncSequence of q; :: thesis: ( dom (compose (p,(q . 1))) = q . 1 & rng (compose (p,(q . 1))) c= q . (len q) )

per cases ( p = {} or p <> {} ) ;

suppose A1: p = {} ; :: thesis: ( dom (compose (p,(q . 1))) = q . 1 & rng (compose (p,(q . 1))) c= q . (len q) )

A2: len q = (len p) + 1 by Def9;
( compose (p,(q . 1)) = id (q . 1) & len p = 0 ) by A1, Th38;
hence ( dom (compose (p,(q . 1))) = q . 1 & rng (compose (p,(q . 1))) c= q . (len q) ) by A2; :: thesis: verum

end;

suppose A3: p <> {} ; :: thesis: ( dom (compose (p,(q . 1))) = q . 1 & rng (compose (p,(q . 1))) c= q . (len q) )

then A4: lastrng p c= q . (len q) by Th65;
( firstdom p = q . 1 & rng (compose (p,(q . 1))) c= lastrng p ) by A3, Th58, Th65;
hence ( dom (compose (p,(q . 1))) = q . 1 & rng (compose (p,(q . 1))) c= q . (len q) ) by A4, Th61; :: thesis: verum

end;

end;