let a be Aleph; :: thesis: ( omega is regular & nextcard a is regular )
thus cf omega = omega by Th34; :: according to CARD_5:def 4 :: thesis: nextcard a is regular
thus cf (nextcard a) = nextcard a by Th35; :: according to CARD_5:def 4 :: thesis: verum