let X be ComplexUnitarySpace; :: thesis: for seq being sequence of X holds 1r * seq = seq
let seq be sequence of X; :: thesis: 1r * seq = seq

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

let n be Element of NAT ; :: thesis: (1r * seq) . n = seq . n
thus (1r * seq) . n = 1r * (seq . n) by CLVECT_1:def 14
.= seq . n by CLVECT_1:def 5 ; :: thesis: verum

end;

hence 1r * seq = seq by FUNCT_2:63; :: thesis: verum