for k, l being Nat holds dom ((f ^\ n) . k) = dom ((f ^\ n) . l)

proof

reconsider g = f as Function of NAT ,(PFuncs X,Y) ;
let k, l be Nat; :: thesis: dom ((f ^\ n) . k) = dom ((f ^\ n) . l)
reconsider k9 = k, l9 = l as Element of NAT by ORDINAL1:def 13;
dom ((f ^\ n) . k) = dom (g . (n + k9)) by NAT_1:def 3;
then dom ((f ^\ n) . k) = dom (g . (n + l9)) by Def2;
hence dom ((f ^\ n) . k) = dom ((f ^\ n) . l) by NAT_1:def 3; :: thesis: verum

end;

hence f ^\ n is with_the_same_dom by Def2; :: thesis: verum