let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2
for v being Vertex of G1 st F is weak_SG-embedding holds
v .degree() c= ((F _V) /. v) .degree()
let F0 be PGraphMapping of G1,G2; :: thesis: for v being Vertex of G1 st F0 is weak_SG-embedding holds
v .degree() c= ((F0 _V) /. v) .degree()
let v be Vertex of G1; :: thesis: ( F0 is weak_SG-embedding implies v .degree() c= ((F0 _V) /. v) .degree() )
assume A1: F0 is weak_SG-embedding ; :: thesis: v .degree() c= ((F0 _V) /. v) .degree()
then F0 _E is one-to-one ;
then consider E being Subset of (the_Edges_of G2) such that
A2: for G3 being reverseEdgeDirections of G2,E ex F being PGraphMapping of G1,G3 st
( F = F0 & F is directed & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) ) by Th93;
set G3 = the reverseEdgeDirections of G2,E;
consider F being PGraphMapping of G1, the reverseEdgeDirections of G2,E such that
A3: ( F = F0 & F is directed ) and
A4: ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) and
( ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) ) by A2;
A5: v .degree() c= ((F _V) /. v) .degree() by A1, A3, A4, Lm5;
dom (F _V) = the_Vertices_of G1 by A1, A4, GLIB_010:def 11;
then A6: ( v in dom (F _V) & v in dom (F0 _V) ) by A3;
(F0 _V) /. v = (F0 _V) . v by A6, PARTFUN1:def 6
.= (F _V) /. v by A3, A6, PARTFUN1:def 6 ;
hence v .degree() c= ((F0 _V) /. v) .degree() by A5, Th60; :: thesis: verum