theorem Th2: :: MATRTOP1:2

for rf1, rf2 being real-valued FinSequence holds sqrt (rf1 ^ rf2) = (sqrt rf1) ^ (sqrt rf2)