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

now

let n be Element of NAT ; :: thesis: (1 * seq) . n = seq . n
thus (1 * seq) . n = 1 * (seq . n) by NORMSP_1:def 8
.= seq . n by RLVECT_1:def 11 ; :: thesis: verum

end;

hence 1 * seq = seq by FUNCT_2:113; :: thesis: verum