let G be _Graph; :: thesis: for f being VColoring of G
for f9 being one-to-one ManySortedSet of rng f st f is proper holds
f9 * f is proper
let f be VColoring of G; :: thesis: for f9 being one-to-one ManySortedSet of rng f st f is proper holds
f9 * f is proper
let f9 be one-to-one ManySortedSet of rng f; :: thesis: ( f is proper implies f9 * f is proper )
rng f c= dom f9 by PARTFUN1:def 2;
hence ( f is proper implies f9 * f is proper ) by Th12; :: thesis: verum