theorem :: NUMBER01:14

for s1, s2 being XFinSequence of NAT
for n being Nat st len s1 = n + 1 & ( for i being Nat st i in dom s1 holds
s1 . i = i |^ 5 ) & len s2 = n + 1 & ( for i being Nat st i in dom s2 holds
s2 . i = i |^ 3 ) holds
Sum s2 divides 3 * (Sum s1)