theorem :: TOPREAL7:14

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))