:: deftheorem Def4 defines |^ VECTSP11:def 4 :
for S being 1-sorted
for F being Function of S,S
for n being Nat
for b₄ being Function of S,S holds
( b₄ = F |^ n iff for F9 being Element of (GFuncs the carrier of S) st F9 = F holds
b₄ = Product (n |-> F9) );