let S be non empty addLoopStr ; :: thesis: for seq1, seq2 being sequence of S holds seq1 - seq2 = seq1 + (- seq2)
let seq1, seq2 be sequence of S; :: thesis: seq1 - seq2 = seq1 + (- seq2)
for n being Element of NAT holds (seq1 - seq2) . n = (seq1 + (- seq2)) . n

proof

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

end;

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