theorem Th1: :: CARD_3:1

for ff being Cardinal-Function holds Card ff = ff