theorem :: TOPREAL7:12

for f, g, h, k being FinSequence of REAL st len f = len h & len g = len k holds
sqr ((f ^ g) + (h ^ k)) = (sqr (f + h)) ^ (sqr (g + k))