let X be ComplexUnitarySpace; :: thesis: for seq1, seq2 being sequence of X
for Cseq being Complex_Sequence holds Cseq * (seq1 + seq2) = (Cseq * seq1) + (Cseq * seq2)
let seq1, seq2 be sequence of X; :: thesis: for Cseq being Complex_Sequence holds Cseq * (seq1 + seq2) = (Cseq * seq1) + (Cseq * seq2)
let Cseq be Complex_Sequence; :: thesis: Cseq * (seq1 + seq2) = (Cseq * seq1) + (Cseq * seq2)

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

let n be Element of NAT ; :: thesis: (Cseq * (seq1 + seq2)) . n = ((Cseq * seq1) + (Cseq * seq2)) . n
thus (Cseq * (seq1 + seq2)) . n = (Cseq . n) * ((seq1 + seq2) . n) by Def8
.= (Cseq . n) * ((seq1 . n) + (seq2 . n)) by NORMSP_1:def 2
.= ((Cseq . n) * (seq1 . n)) + ((Cseq . n) * (seq2 . n)) by CLVECT_1:def 2
.= ((Cseq * seq1) . n) + ((Cseq . n) * (seq2 . n)) by Def8
.= ((Cseq * seq1) . n) + ((Cseq * seq2) . n) by Def8
.= ((Cseq * seq1) + (Cseq * seq2)) . n by NORMSP_1:def 2 ; :: thesis: verum

end;

hence Cseq * (seq1 + seq2) = (Cseq * seq1) + (Cseq * seq2) by FUNCT_2:63; :: thesis: verum