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

now

let x be set ; :: thesis: ( x in NAT implies (seq1 (##) (seq2 + seq3)) . x = ((seq1 (##) seq2) + (seq1 (##) seq3)) . x )
assume x in NAT ; :: thesis: (seq1 (##) (seq2 + seq3)) . x = ((seq1 (##) seq2) + (seq1 (##) seq3)) . x
then reconsider k = x as Element of NAT ;
consider Fr being XFinSequence of REAL such that
A1: dom Fr = k + 1 and
A2: for n being Element of NAT st n in k + 1 holds
Fr . n = (seq1 . n) * ((seq2 + seq3) . (k -' n)) and
A3: Sum Fr = (seq1 (##) (seq2 + seq3)) . k by Def5;
consider Fr1 being XFinSequence of REAL such that
A4: dom Fr1 = k + 1 and
A5: for n being Element of NAT st n in k + 1 holds
Fr1 . n = (seq1 . n) * (seq2 . (k -' n)) and
A6: Sum Fr1 = (seq1 (##) seq2) . k by Def5;
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 Element of NAT st n in k + 1 holds
Fr2 . n = (seq1 . n) * (seq3 . (k -' n)) and
A10: Sum Fr2 = (seq1 (##) seq3) . k by Def5;
A11: for n being Element of NAT st n in dom Fr holds
Fr . n = addreal . (Fr1 . n),(Fr2 . n)

proof

let n be Element of NAT ; :: thesis: ( n in dom Fr implies Fr . n = addreal . (Fr1 . n),(Fr2 . n) )
assume A12: n in dom Fr ; :: thesis: Fr . n = addreal . (Fr1 . n),(Fr2 . n)
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:11;
( 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: verum

end;

len Fr1 = len Fr2 by A4, A8;
then addreal "**" (Fr1 ^ Fr2) = addreal "**" Fr by A11, A7, CARD_FIN:62;
then Sum Fr = addreal . (Sum Fr1),(Sum Fr2) by STIRL2_1:47;
then Sum Fr = (Sum Fr1) + (Sum Fr2) by BINOP_2:def 9;
hence (seq1 (##) (seq2 + seq3)) . x = ((seq1 (##) seq2) + (seq1 (##) seq3)) . x by A3, A6, A10, SEQ_1:11; :: thesis: verum

end;

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