theorem :: MATRIXC1:29

for R being FinSequence of REAL
for F being FinSequence of COMPLEX st R = F & len R >= 1 holds
addreal $$ R = addcomplex $$ F