let X be ComplexUnitarySpace; :: thesis: for seq1, seq2 being sequence of X holds seq1 - seq2 = - (seq2 - seq1)
let seq1, seq2 be sequence of X; :: thesis: seq1 - seq2 = - (seq2 - seq1)

now :: thesis: for n being Element of NAT holds (seq1 - seq2) . n = (- (seq2 - seq1)) . n

let n be Element of NAT ; :: thesis: (seq1 - seq2) . n = (- (seq2 - seq1)) . n
thus (seq1 - seq2) . n = (seq1 . n) - (seq2 . n) by NORMSP_1:def 3
.= - ((seq2 . n) - (seq1 . n)) by RLVECT_1:33
.= - ((seq2 - seq1) . n) by NORMSP_1:def 3
.= (- (seq2 - seq1)) . n by BHSP_1:44 ; :: thesis: verum

end;

hence seq1 - seq2 = - (seq2 - seq1) by FUNCT_2:63; :: thesis: verum