A1: dom (NAT --> 0) = NAT ;

per cases ( k in NAT or not k in NAT ) ;

suppose k in NAT ; :: thesis: (NAT --> 0) . k = 0

hence (NAT --> 0) . k = 0 by FUNCOP_1:7; :: thesis: verum

end;

suppose not k in NAT ; :: thesis: (NAT --> 0) . k = 0

hence (NAT --> 0) . k = 0 by A1, FUNCT_1:def 2; :: thesis: verum

end;

end;