let a, b be Real; :: thesis: for X being RealUnitarySpace
for seq being sequence of X holds (a * b) * seq = a * (b * seq)
let X be RealUnitarySpace; :: 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)
let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: ((a * b) * seq) . n = (a * (b * seq)) . n
thus ((a * b) * seq) . n = (a * b) * (seq . n) by NORMSP_1:def 5
.= a * (b * (seq . n)) by RLVECT_1:def 7
.= a * ((b * seq) . n) by NORMSP_1:def 5
.= (a * (b * seq)) . n by NORMSP_1:def 5 ; :: thesis: verum