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

( 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