let G1, G2 be _Graph; :: thesis: for F being one-to-one PGraphMapping of G1,G2 st F is total holds
card (G1 .loops()) c= card (G2 .loops())
let F be one-to-one PGraphMapping of G1,G2; :: thesis: ( F is total implies card (G1 .loops()) c= card (G2 .loops()) )
assume A1: F is total ; :: thesis: card (G1 .loops()) c= card (G2 .loops())
then reconsider F = F as non empty one-to-one PGraphMapping of G1,G2 ;
A2: (dom F) .loops() = G1 .loops() by A1, Th55, GLIB_009:50;
A3: card ((rng F) .loops()) c= card (G2 .loops()) by GLIB_009:48, CARD_1:11;
card ((dom F) .loops()) c= card ((rng F) .loops()) by Lm4;
hence card (G1 .loops()) c= card (G2 .loops()) by A2, A3, XBOOLE_1:1; :: thesis: verum