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 Th38;
hence dom (compose (p,(firstdom p))) = firstdom p ; :: thesis: verum

end;

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

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

end;

end;