theorem :: VALUED_0:29

for X, Y being non empty set
for s being sequence of X
for h being PartFunc of X,Y
for n being Nat st h is total holds
h /* (s ^\ n) = (h /* s) ^\ n