:: deftheorem dd defines `^ FIELD_16:def 1 :
for L being non empty 1-sorted
for f being Function of L,L
for n being Nat
for b<sub>4</sub> being Function of L,L holds
( b<sub>4</sub> = f `^ n iff ex F being Funcs (b₁,b₁) -valued sequence st
( b₄ = F . n & F . 0 = id L & ( for i being Nat holds F . (i + 1) = (F . i) * f ) ) );