:: deftheorem defines dom GRAPH_1:def 3 :
for C being non empty non void MultiGraphStruct
for f being Edge of C holds dom f = the Source of C . f;