set f = EXP 0;
set g = NAT --> 1;
for n being Element of NAT holds (EXP 0) . n = (NAT --> 1) . n

proof

let n be Element of NAT ; :: thesis: (EXP 0) . n = (NAT --> 1) . n
(EXP 0) . n = n |^ 0 by NAT_5:def 1
.= (NAT --> 1) . n by NEWTON:4 ;
hence (EXP 0) . n = (NAT --> 1) . n ; :: thesis: verum

end;

hence EXP 0 = NAT --> 1 by FUNCT_2:63; :: thesis: verum