let GSeq be GraphSeq; :: thesis: not GSeq is empty
dom GSeq = NAT by PARTFUN1:def 2;
hence not GSeq is empty ; :: thesis: verum