defpred S₁[ FinSequence] means for p being FinSequence of F_Real
for q being real-valued FinSequence st p = q & p = $1 holds
Sum p = Sum q;
A1: S₁[ {} ]

proof

let p be FinSequence of F_Real; :: thesis: for q being real-valued FinSequence st p = q & p = {} holds
Sum p = Sum q
let q be real-valued FinSequence; :: thesis: ( p = q & p = {} implies Sum p = Sum q )
assume A2: ( p = q & p = {} ) ; :: thesis: Sum p = Sum q
then ( p = <*> the carrier of F_Real & q = <*> REAL ) ;
hence Sum p = 0. F_Real by RLVECT_1:43
.= Sum q by A2, RVSUM_1:72 ;
:: thesis: verum

end;

A3: for f being FinSequence
for x being object st S₁[f] holds
S₁[f ^ <*x*>]

proof

let f be FinSequence; :: thesis: for x being object st S₁[f] holds
S₁[f ^ <*x*>]
let x be object ; :: thesis: ( S₁[f] implies S₁[f ^ <*x*>] )
assume A4: S₁[f] ; :: thesis: S₁[f ^ <*x*>]
thus S₁[f ^ <*x*>] :: thesis: verum

proof

let p1 be FinSequence of F_Real; :: thesis: for q being real-valued FinSequence st p1 = q & p1 = f ^ <*x*> holds
Sum p1 = Sum q
let q1 be real-valued FinSequence; :: thesis: ( p1 = q1 & p1 = f ^ <*x*> implies Sum p1 = Sum q1 )
assume A5: ( p1 = q1 & p1 = f ^ <*x*> ) ; :: thesis: Sum p1 = Sum q1
reconsider fp = f as FinSequence of F_Real by A5, FINSEQ_1:36;
rng fp c= REAL ;
then reconsider fq = f as real-valued FinSequence ;
<*x*> is FinSequence of F_Real by A5, FINSEQ_1:36;
then rng <*x*> c= the carrier of F_Real by FINSEQ_1:def 4;
then {x} c= the carrier of F_Real by FINSEQ_1:38;
then reconsider xp = x as Element of F_Real by ZFMISC_1:31;
reconsider xq = xp as Real ;
thus Sum p1 = (Sum fp) + (Sum <*xp*>) by A5, RLVECT_1:41
.= (Sum fp) + xp by RLVECT_1:44
.= (Sum fq) + xq by A4
.= Sum q1 by A5, RVSUM_1:74 ; :: thesis: verum

end;

end;

let p be FinSequence of F_Real; :: thesis: for q being real-valued FinSequence st p = q holds
Sum p = Sum q
let q be real-valued FinSequence; :: thesis: ( p = q implies Sum p = Sum q )
for f being FinSequence holds S₁[f] from FINSEQ_1:sch 3(A1, A3);
hence ( p = q implies Sum p = Sum q ) ; :: thesis: verum