theorem Th4: :: INT_8:4

for s, t being Nat ex r being Nat st (1 + s) |^ t = ((1 + (t * s)) + ((t choose 2) * (s ^2))) + (r * (s ^3))