let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 holds
( F * (id G1) = F & (id G2) * F = F )
let F be PGraphMapping of G1,G2; :: thesis: ( F * (id G1) = F & (id G2) * F = F )
A1: ( dom (F _V) c= the_Vertices_of G1 & dom (F _E) c= the_Edges_of G1 ) ;
thus F * (id G1) = [(F _V),((F _E) * (id (the_Edges_of G1)))] by A1, RELAT_1:51
.= [(F _V),(F _E)] by A1, RELAT_1:51
.= F ; :: thesis: (id G2) * F = F
A2: ( rng (F _V) c= the_Vertices_of G2 & rng (F _E) c= the_Edges_of G2 ) ;
thus (id G2) * F = [(F _V),((id (the_Edges_of G2)) * (F _E))] by A2, RELAT_1:53
.= [(F _V),(F _E)] by A2, RELAT_1:53
.= F ; :: thesis: verum