let G1, G2 be _Graph; :: thesis: ex f, g being Function st
( [{},{}] = [f,g] & dom f c= the_Vertices_of G1 & rng f c= the_Vertices_of G2 & dom g c= the_Edges_of G1 & rng g c= the_Edges_of G2 & ( 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 holds
( e Joins v,w,G1 iff g . e Joins f . v,f . w,G2 ) ) & ( 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 ) )
set f = the empty Function;
take the empty Function ; :: thesis: ex g being Function st
( [{},{}] = [ the empty Function,g] & dom the empty Function c= the_Vertices_of G1 & rng the empty Function c= the_Vertices_of G2 & dom g c= the_Edges_of G1 & rng g c= the_Edges_of G2 & ( for e being object st e in dom g holds
( (the_Source_of G1) . e in dom the empty Function & (the_Target_of G1) . e in dom the empty Function ) ) & ( for e, v, w being object st e in dom g & v in dom the empty Function & w in dom the empty Function holds
( e Joins v,w,G1 iff g . e Joins the empty Function . v, the empty Function . w,G2 ) ) & ( for e, v, w being object st e in dom g & v in dom the empty Function & w in dom the empty Function & e Joins v,w,G1 holds
g . e Joins the empty Function . v, the empty Function . w,G2 ) )
take the empty Function ; :: thesis: ( [{},{}] = [ the empty Function, the empty Function] & dom the empty Function c= the_Vertices_of G1 & rng the empty Function c= the_Vertices_of G2 & dom the empty Function c= the_Edges_of G1 & rng the empty Function c= the_Edges_of G2 & ( for e being object st e in dom the empty Function holds
( (the_Source_of G1) . e in dom the empty Function & (the_Target_of G1) . e in dom the empty Function ) ) & ( for e, v, w being object st e in dom the empty Function & v in dom the empty Function & w in dom the empty Function holds
( e Joins v,w,G1 iff the empty Function . e Joins the empty Function . v, the empty Function . w,G2 ) ) & ( for e, v, w being object st e in dom the empty Function & v in dom the empty Function & w in dom the empty Function & e Joins v,w,G1 holds
the empty Function . e Joins the empty Function . v, the empty Function . w,G2 ) )
thus [{},{}] = [ the empty Function, the empty Function] ; :: thesis: ( dom the empty Function c= the_Vertices_of G1 & rng the empty Function c= the_Vertices_of G2 & dom the empty Function c= the_Edges_of G1 & rng the empty Function c= the_Edges_of G2 & ( for e being object st e in dom the empty Function holds
( (the_Source_of G1) . e in dom the empty Function & (the_Target_of G1) . e in dom the empty Function ) ) & ( for e, v, w being object st e in dom the empty Function & v in dom the empty Function & w in dom the empty Function holds
( e Joins v,w,G1 iff the empty Function . e Joins the empty Function . v, the empty Function . w,G2 ) ) & ( for e, v, w being object st e in dom the empty Function & v in dom the empty Function & w in dom the empty Function & e Joins v,w,G1 holds
the empty Function . e Joins the empty Function . v, the empty Function . w,G2 ) )
thus ( dom the empty Function c= the_Vertices_of G1 & rng the empty Function c= the_Vertices_of G2 & dom the empty Function c= the_Edges_of G1 & rng the empty Function c= the_Edges_of G2 ) by XBOOLE_1:2; :: thesis: ( ( for e being object st e in dom the empty Function holds
( (the_Source_of G1) . e in dom the empty Function & (the_Target_of G1) . e in dom the empty Function ) ) & ( for e, v, w being object st e in dom the empty Function & v in dom the empty Function & w in dom the empty Function holds
( e Joins v,w,G1 iff the empty Function . e Joins the empty Function . v, the empty Function . w,G2 ) ) & ( for e, v, w being object st e in dom the empty Function & v in dom the empty Function & w in dom the empty Function & e Joins v,w,G1 holds
the empty Function . e Joins the empty Function . v, the empty Function . w,G2 ) )
thus ( ( for e being object st e in dom the empty Function holds
( (the_Source_of G1) . e in dom the empty Function & (the_Target_of G1) . e in dom the empty Function ) ) & ( for e, v, w being object st e in dom the empty Function & v in dom the empty Function & w in dom the empty Function holds
( e Joins v,w,G1 iff the empty Function . e Joins the empty Function . v, the empty Function . w,G2 ) ) & ( for e, v, w being object st e in dom the empty Function & v in dom the empty Function & w in dom the empty Function & e Joins v,w,G1 holds
the empty Function . e Joins the empty Function . v, the empty Function . w,G2 ) ) ; :: thesis: verum