let G, G1 be _Graph; :: thesis: for g being EColoring of G
for F being PGraphMapping of G1,G
for g9 being EColoring of G1 st F is weak_SG-embedding & g9 = g * (F _E) & g is proper holds
g9 is proper
let g be EColoring of G; :: thesis: for F being PGraphMapping of G1,G
for g9 being EColoring of G1 st F is weak_SG-embedding & g9 = g * (F _E) & g is proper holds
g9 is proper
let F be PGraphMapping of G1,G; :: thesis: for g9 being EColoring of G1 st F is weak_SG-embedding & g9 = g * (F _E) & g is proper holds
g9 is proper
let g9 be EColoring of G1; :: thesis: ( F is weak_SG-embedding & g9 = g * (F _E) & g is proper implies g9 is proper )
assume A1: ( F is weak_SG-embedding & g9 = g * (F _E) & g is proper ) ; :: thesis: g9 is proper
then ( dom (F _E) = the_Edges_of G1 & F _E is one-to-one ) by GLIB_010:def 11;
hence g9 is proper by A1, Th97; :: thesis: verum