reconsider f = (F _V) | () as PartFunc of (),() by PARTFUN1:10;
reconsider g = (F _E) | () as PartFunc of (),() by PARTFUN1:10;
now :: thesis: ( ( for e being object st e in dom g holds
( () . e in dom f & () . 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,H holds
g . e Joins f . v,f . w,G2 ) )
hereby :: thesis: for e, v, w being object st e in dom g & v in dom f & w in dom f & e Joins v,w,H holds
g . e Joins f . v,f . w,G2
let e be object ; :: thesis: ( e in dom g implies ( () . e in dom f & () . e in dom f ) )
assume e in dom g ; :: thesis: ( () . e in dom f & () . e in dom f )
then A1: ( e in dom (F _E) & e in the_Edges_of H ) by RELAT_1:57;
then ( (the_Source_of G1) . e in dom (F _V) & () . e in dom (F _V) ) by Th5;
then A2: ( (the_Source_of H) . e in dom (F _V) & () . e in dom (F _V) ) by ;
( (the_Source_of H) . e in the_Vertices_of H & () . e in the_Vertices_of H ) by ;
hence ( (the_Source_of H) . e in dom f & () . e in dom f ) by ; :: thesis: verum
end;
let e, v, w be object ; :: thesis: ( e in dom g & v in dom f & w in dom f & e Joins v,w,H implies g . e Joins f . v,f . w,G2 )
assume ( e in dom g & v in dom f & w in dom f ) ; :: thesis: ( e Joins v,w,H implies g . e Joins f . v,f . w,G2 )
then A3: ( e in dom (F _E) & e in the_Edges_of H & v in dom (F _V) & v in the_Vertices_of H & w in dom (F _V) & w in the_Vertices_of H ) by RELAT_1:57;
then A4: ( g . e = (F _E) . e & f . v = (F _V) . v & f . w = (F _V) . w ) by FUNCT_1:49;
assume A5: e Joins v,w,H ; :: thesis: g . e Joins f . v,f . w,G2
( v is set & w is set ) by TARSKI:1;
then e Joins v,w,G1 by ;
hence g . e Joins f . v,f . w,G2 by A3, A4, Th4; :: thesis: verum
end;
hence [((F _V) | ()),((F _E) | ())] is PGraphMapping of H,G2 by Th8; :: thesis: verum