thus dom (createGraph (V,E,S,T)) =
dom <*V,E,S,T*>
by GLIB_000:def 11

.= Seg (len <*V,E,S,T*>) by FINSEQ_1:def 3

.= _GraphSelectors by GLIB_000:1, GLIB_000:def 5, FINSEQ_3:2, FINSEQ_4:76 ; :: according to GLIB_009:def 1 :: thesis: verum

.= Seg (len <*V,E,S,T*>) by FINSEQ_1:def 3

.= _GraphSelectors by GLIB_000:1, GLIB_000:def 5, FINSEQ_3:2, FINSEQ_4:76 ; :: according to GLIB_009:def 1 :: thesis: verum