theorem Th10: :: TOPREAL7:10

for f, g being FinSequence of REAL holds sqr (f ^ g) = (sqr f) ^ (sqr g) by RVSUM_1:144;