take seq1 = (- 1) * seq; :: thesis: for n being Element of NAT holds seq1 . n = - (seq . n)
let n be Element of NAT ; :: thesis: seq1 . n = - (seq . n)
thus seq1 . n = (- 1) * (seq . n) by Def3
.= - (seq . n) by EUCLID:43 ; :: thesis: verum