let G, G1 be _Graph; :: thesis: for t being TColoring of G
for F being PGraphMapping of G1,G
for t9 being TColoring of G1 st F is weak_SG-embedding & t9 = [((t _V) * (F _V)),((t _E) * (F _E))] & t is proper holds
t9 is proper
let t be TColoring of G; :: thesis: for F being PGraphMapping of G1,G
for t9 being TColoring of G1 st F is weak_SG-embedding & t9 = [((t _V) * (F _V)),((t _E) * (F _E))] & t is proper holds
t9 is proper
let F be PGraphMapping of G1,G; :: thesis: for t9 being TColoring of G1 st F is weak_SG-embedding & t9 = [((t _V) * (F _V)),((t _E) * (F _E))] & t is proper holds
t9 is proper
let t9 be TColoring of G1; :: thesis: ( F is weak_SG-embedding & t9 = [((t _V) * (F _V)),((t _E) * (F _E))] & t is proper implies t9 is proper )
assume A1: ( F is weak_SG-embedding & t9 = [((t _V) * (F _V)),((t _E) * (F _E))] & t is proper ) ; :: thesis: t9 is proper
then A2: t9 _V is proper by Th26;
A3: t9 _E is proper by A1, Th98;

now :: thesis: for e, v, w being object st e Joins v,w,G1 holds
(t9 _V) . v <> (t9 _E) . e

let e, v, w be object ; :: thesis: ( e Joins v,w,G1 implies (t9 _V) . v <> (t9 _E) . e )
assume A4: e Joins v,w,G1 ; :: thesis: (t9 _V) . v <> (t9 _E) . e
then e in the_Edges_of G1 by GLIB_000:def 13;
then A5: e in dom (F _E) by A1, GLIB_010:def 11;
( ( (the_Source_of G1) . e = v & (the_Target_of G1) . e = w ) or ( (the_Source_of G1) . e = w & (the_Target_of G1) . e = v ) ) by A4, GLIB_000:def 13;
then A6: ( v in dom (F _V) & w in dom (F _V) ) by A5, GLIB_010:5;
then (F _E) . e Joins (F _V) . v,(F _V) . w,G by A4, A5, GLIB_010:4;
then A7: (t _V) . ((F _V) . v) <> (t _E) . ((F _E) . e) by A1, Th146;
( (t _V) . ((F _V) . v) = (t9 _V) . v & (t _E) . ((F _E) . e) = (t9 _E) . e ) by A1, A5, A6, FUNCT_1:13;
hence (t9 _V) . v <> (t9 _E) . e by A7; :: thesis: verum

end;

hence t9 is proper by A2, A3, Th146; :: thesis: verum