theorem Th2: :: FIB_NUM3:2

for a being non negative Real holds (sqrt a) * (sqrt a) = a