n = dom f by CARD_1:def 7;
hence f | n = f ; :: thesis: verum