let n be Nat; :: thesis: for f1, f2 being n -element complex-valued XFinSequence holds Sum (f1 + f2) = (Sum f1) + (Sum f2)
let f1, f2 be n -element complex-valued XFinSequence; :: thesis: Sum (f1 + f2) = (Sum f1) + (Sum f2)
defpred S₁[ Nat] means for f1, f2 being $1 -element complex-valued XFinSequence holds Sum (f1 + f2) = (Sum f1) + (Sum f2);
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume B1: S₁[k] ; :: thesis: S₁[k + 1]
for f1, f2 being k + 1 -element complex-valued XFinSequence holds Sum (f1 + f2) = (Sum f1) + (Sum f2)

proof

let f1, f2 be k + 1 -element complex-valued XFinSequence; :: thesis: Sum (f1 + f2) = (Sum f1) + (Sum f2)
reconsider F = f1 + f2 as k + 1 -element complex-valued XFinSequence ;
reconsider G = (f1 + f2) | k as k -element complex-valued XFinSequence ;
reconsider g1 = f1 | k as k -element complex-valued XFinSequence ;
reconsider g2 = f2 | k as k -element complex-valued XFinSequence ;
C1: ( dom f1 = k + 1 & dom f2 = k + 1 & dom F = k + 1 ) by CARD_1:def 7;
k + 0 < k + 1 by XREAL_1:6;
then C2: ( k in Segm (len f1) & k in Segm (len f2) & k in Segm (len F) ) by C1, NAT_1:44;
then C3: ( Sum (f1 | (k + 1)) = (Sum g1) + (f1 . k) & Sum (f2 | (k + 1)) = (Sum g2) + (f2 . k) ) by AFINSQ_2:65;
C4: Sum (g1 + g2) = (Sum g1) + (Sum g2) by B1;
Sum F = Sum (F | (k + 1))
.= (Sum G) + (F . k) by C2, AFINSQ_2:65
.= ((Sum g1) + (Sum g2)) + ((f1 + f2) . k) by C4, SFG
.= ((Sum g1) + (Sum g2)) + ((f1 . k) + (f2 . k)) by C2, VALUED_1:def 1
.= (Sum f1) + (Sum f2) by C3 ;
hence Sum (f1 + f2) = (Sum f1) + (Sum f2) ; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

A2: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A2, A1);
hence Sum (f1 + f2) = (Sum f1) + (Sum f2) ; :: thesis: verum