theorem Th5: :: RANDOM_2:5

for X being non empty set
for f being PartFunc of X,REAL holds
( f to_power 2 = (- f) to_power 2 & f to_power 2 = (abs f) to_power 2 )