let G be _Graph; :: thesis: for G1, G2 being Subgraph of G st the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 holds
G1 == G2
let G1, G2 be Subgraph of G; :: thesis: ( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 implies G1 == G2 )
assume that
A1: the_Vertices_of G1 = the_Vertices_of G2 and
A2: the_Edges_of G1 = the_Edges_of G2 ; :: thesis: G1 == G2
A3: ( dom (the_Target_of G1) = the_Edges_of G1 & dom (the_Target_of G2) = the_Edges_of G2 ) by FUNCT_2:def 1;
now :: thesis: for e being object st e in the_Edges_of G1 holds
(the_Target_of G1) . e = (the_Target_of G2) . e
let e be object ; :: thesis: ( e in the_Edges_of G1 implies (the_Target_of G1) . e = (the_Target_of G2) . e )
assume A4: e in the_Edges_of G1 ; :: thesis: (the_Target_of G1) . e = (the_Target_of G2) . e
then (the_Target_of G1) . e = (the_Target_of G) . e by Def32;
hence (the_Target_of G1) . e = (the_Target_of G2) . e by A2, A4, Def32; :: thesis: verum
end;
then A5: the_Target_of G1 = the_Target_of G2 by A2, A3, FUNCT_1:2;
A6: now :: thesis: for e being object st e in the_Edges_of G1 holds
(the_Source_of G1) . e = (the_Source_of G2) . e
let e be object ; :: thesis: ( e in the_Edges_of G1 implies (the_Source_of G1) . e = (the_Source_of G2) . e )
assume A7: e in the_Edges_of G1 ; :: thesis: (the_Source_of G1) . e = (the_Source_of G2) . e
then (the_Source_of G1) . e = (the_Source_of G) . e by Def32;
hence (the_Source_of G1) . e = (the_Source_of G2) . e by A2, A7, Def32; :: thesis: verum
end;
( dom (the_Source_of G1) = the_Edges_of G1 & dom (the_Source_of G2) = the_Edges_of G2 ) by FUNCT_2:def 1;
then the_Source_of G1 = the_Source_of G2 by A2, A6, FUNCT_1:2;
hence G1 == G2 by A1, A2, A5; :: thesis: verum