let X be ComplexUnitarySpace; :: thesis: for seq being sequence of X
for Cseq1, Cseq2 being Complex_Sequence holds (Cseq1 + Cseq2) * seq = (Cseq1 * seq) + (Cseq2 * seq)
let seq be sequence of X; :: thesis: for Cseq1, Cseq2 being Complex_Sequence holds (Cseq1 + Cseq2) * seq = (Cseq1 * seq) + (Cseq2 * seq)
let Cseq1, Cseq2 be Complex_Sequence; :: thesis: (Cseq1 + Cseq2) * seq = (Cseq1 * seq) + (Cseq2 * seq)

now :: thesis: for n being Element of NAT holds ((Cseq1 + Cseq2) * seq) . n = ((Cseq1 * seq) + (Cseq2 * seq)) . n

let n be Element of NAT ; :: thesis: ((Cseq1 + Cseq2) * seq) . n = ((Cseq1 * seq) + (Cseq2 * seq)) . n
thus ((Cseq1 + Cseq2) * seq) . n = ((Cseq1 + Cseq2) . n) * (seq . n) by Def8
.= ((Cseq1 . n) + (Cseq2 . n)) * (seq . n) by VALUED_1:1
.= ((Cseq1 . n) * (seq . n)) + ((Cseq2 . n) * (seq . n)) by CLVECT_1:def 3
.= ((Cseq1 * seq) . n) + ((Cseq2 . n) * (seq . n)) by Def8
.= ((Cseq1 * seq) . n) + ((Cseq2 * seq) . n) by Def8
.= ((Cseq1 * seq) + (Cseq2 * seq)) . n by NORMSP_1:def 2 ; :: thesis: verum

end;

hence (Cseq1 + Cseq2) * seq = (Cseq1 * seq) + (Cseq2 * seq) by FUNCT_2:63; :: thesis: verum