let n be Nat; :: thesis: for t, z being Integer st t divides (t + z) |^ n holds
t divides ((t + z) |^ n) + (z |^ n)
let t, z be Integer; :: thesis: ( t divides (t + z) |^ n implies t divides ((t + z) |^ n) + (z |^ n) )
assume A0: t divides (t + z) |^ n ; :: thesis: t divides ((t + z) |^ n) + (z |^ n)
then t divides z |^ n by Th11;
hence t divides ((t + z) |^ n) + (z |^ n) by WSIERP_1:4, A0; :: thesis: verum