let a, b be Complex; :: thesis: for X being ComplexUnitarySpace
for seq being sequence of X holds (a * b) * seq = a * (b * seq)
let X be ComplexUnitarySpace; :: thesis: for seq being sequence of X holds (a * b) * seq = a * (b * seq)
let seq be sequence of X; :: thesis: (a * b) * seq = a * (b * seq)

now :: thesis: for n being Element of NAT holds ((a * b) * seq) . n = (a * (b * seq)) . n

let n be Element of NAT ; :: thesis: ((a * b) * seq) . n = (a * (b * seq)) . n
thus ((a * b) * seq) . n = (a * b) * (seq . n) by CLVECT_1:def 14
.= a * (b * (seq . n)) by CLVECT_1:def 4
.= a * ((b * seq) . n) by CLVECT_1:def 14
.= (a * (b * seq)) . n by CLVECT_1:def 14 ; :: thesis: verum

end;

hence (a * b) * seq = a * (b * seq) by FUNCT_2:63; :: thesis: verum