let V be non empty set ; :: thesis: for E being Relation of V holds rng E = rng (the_Target_of (createGraph (V,E)))
let E be Relation of V; :: thesis: rng E = rng (the_Target_of (createGraph (V,E)))
now :: thesis: for w being object holds
( ( w in rng E implies w in rng (the_Target_of (createGraph (V,E))) ) & ( w in rng (the_Target_of (createGraph (V,E))) implies w in rng E ) )
let w be object ; :: thesis: ( ( w in rng E implies w in rng (the_Target_of (createGraph (V,E))) ) & ( w in rng (the_Target_of (createGraph (V,E))) implies w in rng E ) )
hereby :: thesis: ( w in rng (the_Target_of (createGraph (V,E))) implies w in rng E )
assume w in rng E ; :: thesis: w in rng (the_Target_of (createGraph (V,E)))
then consider v being object such that
A1: [v,w] in E by XTUPLE_0:def 13;
[v,w] DJoins v,w, createGraph (V,E) by A1, Th63;
then A2: ( [v,w] in the_Edges_of (createGraph (V,E)) & (the_Target_of (createGraph (V,E))) . [v,w] = w ) by GLIB_000:def 14;
then [v,w] in dom (the_Target_of (createGraph (V,E))) by FUNCT_2:def 1;
hence w in rng (the_Target_of (createGraph (V,E))) by A2, FUNCT_1:3; :: thesis: verum
end;
assume w in rng (the_Target_of (createGraph (V,E))) ; :: thesis: w in rng E
then consider e being object such that
A3: ( e in dom (the_Target_of (createGraph (V,E))) & (the_Target_of (createGraph (V,E))) . e = w ) by FUNCT_1:def 3;
A4: e in the_Edges_of (createGraph (V,E)) by A3;
set v = (the_Source_of (createGraph (V,E))) . e;
e DJoins (the_Source_of (createGraph (V,E))) . e,w, createGraph (V,E) by A3, GLIB_000:def 14;
then A5: e = [((the_Source_of (createGraph (V,E))) . e),w] by Th64;
e in E by A4;
hence w in rng E by A5, XTUPLE_0:def 13; :: thesis: verum
end;
hence rng E = rng (the_Target_of (createGraph (V,E))) by TARSKI:2; :: thesis: verum