let s be set ; :: thesis: for i being Nat
for R1, R2 being b₁ -element FinSequence of COMPLEX holds (R1 + R2) . s = (R1 . s) + (R2 . s)
let i be Nat; :: thesis: for R1, R2 being i -element FinSequence of COMPLEX holds (R1 + R2) . s = (R1 . s) + (R2 . s)
let R1, R2 be i -element FinSequence of COMPLEX ; :: thesis: (R1 + R2) . s = (R1 . s) + (R2 . s)

per cases ( not s in Seg i or s in Seg i ) ;

suppose A1: not s in Seg i ; :: thesis: (R1 + R2) . s = (R1 . s) + (R2 . s)

then A2: not s in dom R2 by FINSEQ_2:124;
A3: not s in dom R1 by A1, FINSEQ_2:124;
not s in dom (R1 + R2) by A1, FINSEQ_2:124;
hence (R1 + R2) . s = 0 + 0 by FUNCT_1:def 2
.= (R1 . s) + 0 by A3, FUNCT_1:def 2
.= (R1 . s) + (R2 . s) by A2, FUNCT_1:def 2 ;
:: thesis: verum

end;

suppose s in Seg i ; :: thesis: (R1 + R2) . s = (R1 . s) + (R2 . s)

then s in dom (R1 + R2) by FINSEQ_2:124;
hence (R1 + R2) . s = (R1 . s) + (R2 . s) by VALUED_1:def 1; :: thesis: verum

end;

end;