let V be non empty set ; :: thesis: for E being Relation of V holds dom E = rng (the_Source_of (createGraph (V,E)))
let E be Relation of V; :: thesis: dom E = rng (the_Source_of (createGraph (V,E)))

now :: thesis: for v being object holds
( ( v in dom E implies v in rng (the_Source_of (createGraph (V,E))) ) & ( v in rng (the_Source_of (createGraph (V,E))) implies v in dom E ) )

let v be object ; :: thesis: ( ( v in dom E implies v in rng (the_Source_of (createGraph (V,E))) ) & ( v in rng (the_Source_of (createGraph (V,E))) implies v in dom E ) )

hereby :: thesis: ( v in rng (the_Source_of (createGraph (V,E))) implies v in dom E )

assume v in dom E ; :: thesis: v in rng (the_Source_of (createGraph (V,E)))
then consider w being object such that
A1: [v,w] in E by XTUPLE_0:def 12;
[v,w] DJoins v,w, createGraph (V,E) by A1, Th63;
then A2: ( [v,w] in the_Edges_of (createGraph (V,E)) & (the_Source_of (createGraph (V,E))) . [v,w] = v ) by GLIB_000:def 14;
then [v,w] in dom (the_Source_of (createGraph (V,E))) by FUNCT_2:def 1;
hence v in rng (the_Source_of (createGraph (V,E))) by A2, FUNCT_1:3; :: thesis: verum

end;

assume v in rng (the_Source_of (createGraph (V,E))) ; :: thesis: v in dom E
then consider e being object such that
A3: ( e in dom (the_Source_of (createGraph (V,E))) & (the_Source_of (createGraph (V,E))) . e = v ) by FUNCT_1:def 3;
A4: e in the_Edges_of (createGraph (V,E)) by A3;
set w = (the_Target_of (createGraph (V,E))) . e;
e DJoins v,(the_Target_of (createGraph (V,E))) . e, createGraph (V,E) by A3, GLIB_000:def 14;
then A5: e = [v,((the_Target_of (createGraph (V,E))) . e)] by Th64;
e in E by A4;
hence v in dom E by A5, XTUPLE_0:def 12; :: thesis: verum

end;

hence dom E = rng (the_Source_of (createGraph (V,E))) by TARSKI:2; :: thesis: verum