let seq1, seq2, seq3 be Complex_Sequence; :: thesis: (seq1 + seq2) (#) seq3 = (seq1 (#) seq3) + (seq2 (#) seq3)

now :: thesis: for n being Element of NAT holds ((seq1 + seq2) (#) seq3) . n = ((seq1 (#) seq3) + (seq2 (#) seq3)) . n

let n be Element of NAT ; :: thesis: ((seq1 + seq2) (#) seq3) . n = ((seq1 (#) seq3) + (seq2 (#) seq3)) . n
thus ((seq1 + seq2) (#) seq3) . n = ((seq1 + seq2) . n) * (seq3 . n) by VALUED_1:5
.= ((seq1 . n) + (seq2 . n)) * (seq3 . n) by VALUED_1:1
.= ((seq1 . n) * (seq3 . n)) + ((seq2 . n) * (seq3 . n))
.= ((seq1 (#) seq3) . n) + ((seq2 . n) * (seq3 . n)) by VALUED_1:5
.= ((seq1 (#) seq3) . n) + ((seq2 (#) seq3) . n) by VALUED_1:5
.= ((seq1 (#) seq3) + (seq2 (#) seq3)) . n by VALUED_1:1 ; :: thesis: verum

end;

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