let G, G1 be _Graph; :: thesis: for t being TColoring of G
for F being PGraphMapping of G1,G st F is total holds
[((t _V) * (F _V)),((t _E) * (F _E))] is TColoring of G1
let t be TColoring of G; :: thesis: for F being PGraphMapping of G1,G st F is total holds
[((t _V) * (F _V)),((t _E) * (F _E))] is TColoring of G1
let F be PGraphMapping of G1,G; :: thesis: ( F is total implies [((t _V) * (F _V)),((t _E) * (F _E))] is TColoring of G1 )
assume A1: F is total ; :: thesis: [((t _V) * (F _V)),((t _E) * (F _E))] is TColoring of G1
then A2: (t _V) * (F _V) is VColoring of G1 by Th9;
(t _E) * (F _E) is EColoring of G1 by A1, Th84;
hence [((t _V) * (F _V)),((t _E) * (F _E))] is TColoring of G1 by A2, Def9; :: thesis: verum