theorem finex: :: REALALG3:2

for F being Field
for E being FieldExtension of F
for f being FinSequence of E st ( for i being Nat st i in dom f holds
f . i in F ) holds
( f is FinSequence of F & Sum f in F )