:: deftheorem Def2 defines repeat GRAPHSP:def 2 :
for X being set
for f being Element of Funcs (X,X)
for b₃ being sequence of (Funcs (X,X)) holds
( b₃ = repeat f iff ( b₃ . 0 = id X & ( for i being Nat holds b₃ . (i + 1) = f * (b₃ . i) ) ) );