let k be Nat; :: thesis: for a being non trivial Nat st Py (a,k) = 0 holds
k = 0
let a be non trivial Nat; :: thesis: ( Py (a,k) = 0 implies k = 0 )
assume Py (a,k) = 0 ; :: thesis: k = 0
then Py (a,k) = Py (a,0) by Th6;
hence k = 0 by Th15; :: thesis: verum