A1:
card INT c= card (NAT \/ [:{0},NAT:])
by CARD_1:11, NUMBERS:def 4;
A2:
card [:NAT,{0}:] = card [:{0},NAT:]
by CARD_2:4;
A3:
card [:NAT,{0}:] = card NAT
by CARD_1:69;
omega +` omega = omega
by CARD_2:75;
then
card (NAT \/ [:{0},NAT:]) c= omega
by A3, A2, CARD_2:34;
hence
card INT c= omega
by A1; XBOOLE_0:def 10 omega c= card INT
thus
omega c= card INT
by CARD_1:11, CARD_1:47, NUMBERS:17; verum