theorem Th15: :: TOPREAL7:15

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