let X be RealUnitarySpace; :: thesis: for seq being sequence of X holds seq = seq - (0. X)
let seq be sequence of X; :: thesis: seq = seq - (0. X)
let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: seq . n = (seq - (0. X)) . n
thus (seq - H₁(X)) . n = (seq . n) - H₁(X) by NORMSP_1:def 4
.= seq . n by RLVECT_1:13 ; :: thesis: verum