let a be Complex; :: thesis: for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X holds a * (seq1 - seq2) = (a * seq1) - (a * seq2)
let X be ComplexUnitarySpace; :: thesis: for seq1, seq2 being sequence of X holds a * (seq1 - seq2) = (a * seq1) - (a * seq2)
let seq1, seq2 be sequence of X; :: thesis: a * (seq1 - seq2) = (a * seq1) - (a * seq2)

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

let n be Element of NAT ; :: thesis: (a * (seq1 - seq2)) . n = ((a * seq1) - (a * seq2)) . n
thus (a * (seq1 - seq2)) . n = a * ((seq1 - seq2) . n) by CLVECT_1:def 14
.= a * ((seq1 . n) - (seq2 . n)) by NORMSP_1:def 3
.= (a * (seq1 . n)) - (a * (seq2 . n)) by CLVECT_1:9
.= ((a * seq1) . n) - (a * (seq2 . n)) by CLVECT_1:def 14
.= ((a * seq1) . n) - ((a * seq2) . n) by CLVECT_1:def 14
.= ((a * seq1) - (a * seq2)) . n by NORMSP_1:def 3 ; :: thesis: verum

end;

hence a * (seq1 - seq2) = (a * seq1) - (a * seq2) by FUNCT_2:63; :: thesis: verum