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