let p be FuncSequence; :: thesis: dom (compose p,(firstdom p)) = firstdom p

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

suppose p = {} ; :: thesis: dom (compose p,(firstdom p)) = firstdom p

then compose p,(firstdom p) = id (firstdom p) by Th41;
hence dom (compose p,(firstdom p)) = firstdom p by RELAT_1:71; :: thesis: verum

end;

suppose p <> {} ; :: thesis: dom (compose p,(firstdom p)) = firstdom p

then dom (compose p,(firstdom p)) = (firstdom p) /\ (firstdom p) by Th63;
hence dom (compose p,(firstdom p)) = firstdom p ; :: thesis: verum

end;

end;