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

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