let x be Real; :: thesis: x #Z 2 = x ^2
x #Z 2 = x |^ 2 by PREPOWER:36
.= x ^2 by NEWTON:81 ;
hence x #Z 2 = x ^2 ; :: thesis: verum