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

proof

let n be Element of NAT ; :: thesis: (EXP 1) . n = (id NAT) . n
(EXP 1) . n = n |^ 1 by NAT_5:def 1
.= (id NAT) . n ;
hence (EXP 1) . n = (id NAT) . n ; :: thesis: verum

end;

hence EXP 1 = id NAT by FUNCT_2:63; :: thesis: verum