let X be Function; :: thesis: ( X = _E implies ( X is the_Edges_of G1 -defined & X is the_Edges_of G2 -valued ) )

assume A4: X = _E ; :: thesis: ( X is the_Edges_of G1 -defined & X is the_Edges_of G2 -valued )

consider f, g being Function such that

A5: F = [f,g] and

( dom f c= the_Vertices_of G1 & rng f c= the_Vertices_of G2 ) and

A6: ( dom g c= the_Edges_of G1 & rng g c= the_Edges_of G2 ) and

( ( for e being object st e in dom g holds

( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) ) & ( for e, v, w being object st e in dom g & v in dom f & w in dom f & e Joins v,w,G1 holds

g . e Joins f . v,f . w,G2 ) ) by Def8;

thus ( X is the_Edges_of G1 -defined & X is the_Edges_of G2 -valued ) by A4, A5, A6, RELAT_1:def 18, RELAT_1:def 19; :: thesis: verum

assume A4: X = _E ; :: thesis: ( X is the_Edges_of G1 -defined & X is the_Edges_of G2 -valued )

consider f, g being Function such that

A5: F = [f,g] and

( dom f c= the_Vertices_of G1 & rng f c= the_Vertices_of G2 ) and

A6: ( dom g c= the_Edges_of G1 & rng g c= the_Edges_of G2 ) and

( ( for e being object st e in dom g holds

( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) ) & ( for e, v, w being object st e in dom g & v in dom f & w in dom f & e Joins v,w,G1 holds

g . e Joins f . v,f . w,G2 ) ) by Def8;

thus ( X is the_Edges_of G1 -defined & X is the_Edges_of G2 -valued ) by A4, A5, A6, RELAT_1:def 18, RELAT_1:def 19; :: thesis: verum