let G1, G2 be _Graph; :: thesis: for F being non empty one-to-one PGraphMapping of G1,G2 holds card ((dom F) .loops()) = card ((rng F) .loops())
let F be non empty one-to-one PGraphMapping of G1,G2; :: thesis: card ((dom F) .loops()) = card ((rng F) .loops())
reconsider F2 = F " as non empty one-to-one PGraphMapping of G2,G1 ;
A1: ( card ((dom F) .loops()) c= card ((rng F) .loops()) & card ((dom F2) .loops()) c= card ((rng F2) .loops()) ) by Lm4;
( dom F2 = rng F & rng F2 = dom F ) by Th81;
hence card ((dom F) .loops()) = card ((rng F) .loops()) by A1, XBOOLE_0:def 10; :: thesis: verum