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 k' = k, l' = l as Element of NAT by ORDINAL1:def 13;
dom ((f ^\ n) . k) = dom (g . (n + k')) by NAT_1:def 3;
then dom ((f ^\ n) . k) = dom (g . (n + l')) 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