per cases ( X is empty or not X is empty ) ;
suppose X is empty ; :: thesis: NatMinor f is finite
then NatMinor f c= Funcs ({},NAT) ;
then NatMinor f c= {{}} by FUNCT_5:57;
hence NatMinor f is finite ; :: thesis: verum
end;
suppose not X is empty ; :: thesis: NatMinor f is finite
then reconsider X = X as non empty set ;
reconsider f = f as finite-support Function of X,NAT ;
card (NatMinor f) = multnat $$ ((support f),(addnat [:] (f,1))) by Th61;
hence NatMinor f is finite ; :: thesis: verum
end;
end;