let G be _Graph; :: thesis: G .loops() = dom ((the_Source_of G) /\ (the_Target_of G))

now :: thesis: for e being object holds
( ( e in G .loops() implies e in dom ((the_Source_of G) /\ (the_Target_of G)) ) & ( e in dom ((the_Source_of G) /\ (the_Target_of G)) implies e in G .loops() ) )

let e be object ; :: thesis: ( ( e in G .loops() implies e in dom ((the_Source_of G) /\ (the_Target_of G)) ) & ( e in dom ((the_Source_of G) /\ (the_Target_of G)) implies e in G .loops() ) )

hereby :: thesis: ( e in dom ((the_Source_of G) /\ (the_Target_of G)) implies e in G .loops() )

assume e in G .loops() ; :: thesis: e in dom ((the_Source_of G) /\ (the_Target_of G))
then consider v being object such that
A1: e DJoins v,v,G by GLIB_009:45;
e in the_Edges_of G by A1, GLIB_000:def 14;
then A2: ( e in dom (the_Source_of G) & e in dom (the_Target_of G) ) by FUNCT_2:def 1;
( (the_Source_of G) . e = v & (the_Target_of G) . e = v ) by A1, GLIB_000:def 14;
then ( [e,v] in the_Source_of G & [e,v] in the_Target_of G ) by A2, FUNCT_1:def 2;
then [e,v] in (the_Source_of G) /\ (the_Target_of G) by XBOOLE_0:def 4;
hence e in dom ((the_Source_of G) /\ (the_Target_of G)) by FUNCT_1:1; :: thesis: verum

end;

set v = ((the_Source_of G) /\ (the_Target_of G)) . e;
assume e in dom ((the_Source_of G) /\ (the_Target_of G)) ; :: thesis: e in G .loops()
then [e,(((the_Source_of G) /\ (the_Target_of G)) . e)] in (the_Source_of G) /\ (the_Target_of G) by FUNCT_1:def 2;
then A3: ( [e,(((the_Source_of G) /\ (the_Target_of G)) . e)] in the_Source_of G & [e,(((the_Source_of G) /\ (the_Target_of G)) . e)] in the_Target_of G ) by XBOOLE_0:def 4;
then A4: ( e in dom (the_Source_of G) & e in dom (the_Target_of G) ) by FUNCT_1:1;
then ( (the_Source_of G) . e = ((the_Source_of G) /\ (the_Target_of G)) . e & (the_Target_of G) . e = ((the_Source_of G) /\ (the_Target_of G)) . e ) by A3, FUNCT_1:def 2;
hence e in G .loops() by A4, GLIB_000:def 14, GLIB_009:45; :: thesis: verum

end;

hence G .loops() = dom ((the_Source_of G) /\ (the_Target_of G)) by TARSKI:2; :: thesis: verum