theorem Th1: :: SIMPLEX1:1

for X being set
for R being Relation
for C being Cardinal st ( for x being object st x in X holds
card (Im (R,x)) = C ) holds
card R = (card (R | ((dom R) \ X))) +` (C *` (card X))