let x be object ; :: according to VALUED_0:def 12 :: thesis: ( not x in dom (b |^ n) or not (b |^ n) . x is natural )
set f = b |^ n;
assume x in dom (b |^ n) ; :: thesis: (b |^ n) . x is natural
(b |^ n) . x = (b . x) |^ n by Def6;
hence (b |^ n) . x is natural ; :: thesis: verum