let X be RealUnitarySpace; :: thesis: for x being Point of X
for seq being sequence of X holds seq - x = seq + (- x)
let x be Point of X; :: thesis: for seq being sequence of X holds seq - x = seq + (- x)
let seq be sequence of X; :: thesis: seq - x = seq + (- x)
let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: (seq - x) . n = (seq + (- x)) . n
thus (seq - x) . n = (seq . n) - x by NORMSP_1:def 4
.= (seq + (- x)) . n by Def6 ; :: thesis: verum