let X be ComplexUnitarySpace; :: 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)

now :: thesis: for n being Element of NAT holds (seq - x) . n = (seq + (- x)) . n

let n be Element of NAT ; :: thesis: (seq - x) . n = (seq + (- x)) . n
thus (seq - x) . n = (seq . n) - x by NORMSP_1:def 4
.= (seq + (- x)) . n by BHSP_1:def 6 ; :: thesis: verum

end;

hence seq - x = seq + (- x) by FUNCT_2:63; :: thesis: verum