let G1, G2 be _Graph; :: thesis: for c being Cardinal
for F being PGraphMapping of G1,G2 st F is weak_SG-embedding & G2 is c -vcolorable holds
G1 is c -vcolorable
let c be Cardinal; :: thesis: for F being PGraphMapping of G1,G2 st F is weak_SG-embedding & G2 is c -vcolorable holds
G1 is c -vcolorable
let F be PGraphMapping of G1,G2; :: thesis: ( F is weak_SG-embedding & G2 is c -vcolorable implies G1 is c -vcolorable )
assume A1: ( F is weak_SG-embedding & G2 is c -vcolorable ) ; :: thesis: G1 is c -vcolorable
then consider f2 being VColoring of G2 such that
A2: ( f2 is proper & card (rng f2) c= c ) ;
reconsider f1 = f2 * (F _V) as VColoring of G1 by A1, Th9;
card (rng f1) c= card (rng f2) by RELAT_1:26, CARD_1:11;
then card (rng f1) c= c by A2, XBOOLE_1:1;
hence G1 is c -vcolorable by A1, A2, Th26; :: thesis: verum