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 p = {} ; :: thesis: ( dom (compose p,(q . 1)) = q . 1 & rng (compose p,(q . 1)) c= q . (len q) )

then ( compose p,(q . 1) = id (q . 1) & len p = 0 & len q = (len p) + 1 ) by Def10, Th41;
hence ( dom (compose p,(q . 1)) = q . 1 & rng (compose p,(q . 1)) c= q . (len q) ) by RELAT_1:71; :: thesis: verum

end;

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

then ( firstdom p = q . 1 & rng (compose p,(q . 1)) c= lastrng p & lastrng p c= q . (len q) ) by Th61, Th68;
hence ( dom (compose p,(q . 1)) = q . 1 & rng (compose p,(q . 1)) c= q . (len q) ) by Th64, XBOOLE_1:1; :: thesis: verum

end;

end;