:: deftheorem defines are_fiberwise_equipotent CLASSES1:def 10 :
for F, G being Relation holds
( F,G are_fiberwise_equipotent iff for x being object holds card (Coim (F,x)) = card (Coim (G,x)) );