for F being FinSequence of COMPLEX
for x being Element of COMPLEX holds Re (F ^ <*x*>) = (Re F) ^ <*(Re x)*>