let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 holds
( F | (dom F) = F & (rng F) |` F = F )
let F be PGraphMapping of G1,G2; :: thesis: ( F | (dom F) = F & (rng F) |` F = F )

per cases ( not F is empty or F is empty ) ;

suppose A1: not F is empty ; :: thesis: ( F | (dom F) = F & (rng F) |` F = F )

A2: (F | (dom F)) _V = (F _V) | (dom (F _V)) by A1, GLIB_010:54
.= F _V ;
(F | (dom F)) _E = (F _E) | (dom (F _E)) by A1, GLIB_010:54
.= F _E ;
then [((F | (dom F)) _V),((F | (dom F)) _E)] = [(F _V),(F _E)] by A2;
hence F | (dom F) = F ; :: thesis: (rng F) |` F = F
A3: ((rng F) |` F) _V = (rng (F _V)) |` (F _V) by A1, GLIB_010:54
.= F _V ;
((rng F) |` F) _E = (rng (F _E)) |` (F _E) by A1, GLIB_010:54
.= F _E ;
then [(((rng F) |` F) _V),(((rng F) |` F) _E)] = [(F _V),(F _E)] by A3;
hence (rng F) |` F = F ; :: thesis: verum

end;

suppose A4: F is empty ; :: thesis: ( F | (dom F) = F & (rng F) |` F = F )

hence F | (dom F) = F by Th85; :: thesis: (rng F) |` F = F
thus (rng F) |` F = F by A4, Th85; :: thesis: verum

end;

end;