let F be Field; :: thesis: 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 )
let E be FieldExtension of F; :: thesis: 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 )
let f be FinSequence of E; :: thesis: ( ( for i being Nat st i in dom f holds
f . i in F ) implies ( f is FinSequence of F & Sum f in F ) )
assume AS: for i being Nat st i in dom f holds
f . i in F ; :: thesis: ( f is FinSequence of F & Sum f in F )
I1: F is Subring of E by FIELD_4:def 1;

per cases ( len f = 0 or len f > 0 ) ;

suppose len f = 0 ; :: thesis: ( f is FinSequence of F & Sum f in F )

then A: f = <*> the carrier of F ;
then Sum f = Sum (<*> the carrier of F) by I1, FIELD_4:2
.= 0. F by RLVECT_1:43 ;
hence ( f is FinSequence of F & Sum f in F ) by A; :: thesis: verum

end;

suppose len f > 0 ; :: thesis: ( f is FinSequence of F & Sum f in F )

then f <> {} ;
then consider G being FinSequence, y being object such that
B2: f = G ^ <*y*> by FINSEQ_1:46;
rng G c= rng f by B2, FINSEQ_1:29;
then reconsider G = G as FinSequence of E by XBOOLE_1:1, FINSEQ_1:def 4;
C: dom G c= dom f by B2, FINSEQ_1:26;

D: now :: thesis: for i being Nat st i in dom G holds
G . i in F

let i be Nat; :: thesis: ( i in dom G implies G . i in F )
assume C0: i in dom G ; :: thesis: G . i in F
then G . i = f . i by B2, FINSEQ_1:def 7;
hence G . i in F by C, C0, AS; :: thesis: verum

end;

now :: thesis: for o being object st o in rng G holds
o in the carrier of F

let o be object ; :: thesis: ( o in rng G implies o in the carrier of F )
assume o in rng G ; :: thesis: o in the carrier of F
then consider u being object such that
D1: ( u in dom G & G . u = o ) by FUNCT_1:def 3;
reconsider u = u as Element of NAT by D1;
o in F by D, D1;
hence o in the carrier of F ; :: thesis: verum

end;

then rng G c= the carrier of F ;
then reconsider G = G as FinSequence of F by FINSEQ_1:def 4;
rng <*y*> = {y} by FINSEQ_1:39;
then G5: y in rng <*y*> by TARSKI:def 1;
rng <*y*> c= rng f by B2, FINSEQ_1:30;
then consider u being object such that
G6: ( u in dom f & f . u = y ) by G5, FUNCT_1:def 3;
reconsider u = u as Element of NAT by G6;
f . u in F by AS, G6;
then reconsider y = y as Element of F by G6;
B4: ( <*y*> is FinSequence of F & G is FinSequence of F & f = G ^ <*y*> ) by B2;
Sum f = Sum (G ^ <*y*>) by I1, FIELD_4:2, B2
.= (Sum G) + (Sum <*y*>) by RLVECT_1:41
.= (Sum G) + y by RLVECT_1:44 ;
hence ( f is FinSequence of F & Sum f in F ) by B4; :: thesis: verum

end;

end;