theorem :: NUMBER15:71

for s, n being positive Nat
for f being Solution_of_Sierp168 of s holds n (#) f is Solution_of_Sierp168 of s by Def14;