theorem Th1: :: FDIFF_7:1

for x being Real holds x #Z 2 = x ^2