theorem T3: :: FIELD_16:2

for L being non empty 1-sorted
for f being Function of L,L
for n being Nat holds
( f `^ (n + 1) = (f `^ n) * f & (f `^ n) * f = f * (f `^ n) )