theorem Th4: :: AOFA_I00:4

for X, N, I being non empty set
for s being Function of X,I
for c being Function of X,N st c is one-to-one holds
for n being Element of I holds (N --> n) +* (s * (c ")) is Function of N,I