let seq1, seq2, seq3 be Real_Sequence; :: thesis:
set S = seq2 + seq3;
set S2 = seq1 (##) seq2;
set S3 = seq1 (##) seq3;

now :: thesis:

let x be object ; :: thesis:
assume x in NAT ; :: thesis:
then reconsider k = x as Nat ;
consider Fr being XFinSequence of REAL such that
A1: dom Fr = k + 1 and
A2: for n being Nat st n in k + 1 holds
Fr . n = (seq1 . n) * ((seq2 + seq3) . (k -' n)) and
A3: Sum Fr = (seq1 (##) (seq2 + seq3)) . k by Def4;
consider Fr1 being XFinSequence of REAL such that
A4: dom Fr1 = k + 1 and
A5: for n being Nat st n in k + 1 holds
Fr1 . n = (seq1 . n) * (seq2 . (k -' n)) and
A6: Sum Fr1 = (seq1 (##) seq2) . k by Def4;
A7: len Fr1 = len Fr by A1, A4;
consider Fr2 being XFinSequence of REAL such that
A8: dom Fr2 = k + 1 and
A9: for n being Nat st n in k + 1 holds
Fr2 . n = (seq1 . n) * (seq3 . (k -' n)) and
A10: Sum Fr2 = (seq1 (##) seq3) . k by Def4;
A11: for n being Nat st n in dom Fr holds
Fr . n = addreal . ((Fr1 . n),(Fr2 . n))

proof

let n be Nat; :: thesis:
assume A12: n in dom Fr ; :: thesis:
A13: Fr . n = (seq1 . n) * ((seq2 + seq3) . (k -' n)) by A1, A2, A12;
A14: (seq2 + seq3) . (k -' n) = (seq2 . (k -' n)) + (seq3 . (k -' n)) by SEQ_1:7;
( Fr1 . n = (seq1 . n) * (seq2 . (k -' n)) & Fr2 . n = (seq1 . n) * (seq3 . (k -' n)) ) by A1, A5, A9, A12;
then Fr . n = (Fr1 . n) + (Fr2 . n) by A13, A14;
hence Fr . n = addreal . ((Fr1 . n),(Fr2 . n)) by BINOP_2:def 9; :: thesis:

end;

len Fr1 = len Fr2 by A4, A8;
then addreal "**" (Fr1 ^ Fr2) = addreal "**" Fr by A11, A7, AFINSQ_2:46;
then Sum Fr = addreal "**" (Fr1 ^ Fr2) by AFINSQ_2:48;
then Sum Fr = Sum (Fr1 ^ Fr2) by AFINSQ_2:48;
then Sum Fr = (Sum Fr1) + (Sum Fr2) by AFINSQ_2:55;
hence (seq1 (##) (seq2 + seq3)) . x = ((seq1 (##) seq2) + (seq1 (##) seq3)) . x by A3, A6, A10, SEQ_1:7; :: thesis:

end;

hence seq1 (##) (seq2 + seq3) = (seq1 (##) seq2) + (seq1 (##) seq3) by FUNCT_2:12; :: thesis: