let F1, F2 be Graph-yielding Function; :: thesis: ( F1,F2 are_isomorphic implies card F1 = card F2 )
assume F1,F2 are_isomorphic ; :: thesis: card F1 = card F2
then consider p being one-to-one Function such that
A1: ( dom p = dom F1 & rng p = dom F2 ) and
for x being object st x in dom F1 holds
ex G1, G2 being _Graph st
( G1 = F1 . x & G2 = F2 . (p . x) & G2 is G1 -isomorphic ) ;
thus card F1 = card (dom F1) by CARD_1:62
.= card (dom F2) by A1, CARD_1:70
.= card F2 by CARD_1:62 ; :: thesis: verum