let seq1, seq be Real_Sequence; :: thesis: ( - (seq1 /" seq) = (- seq1) /" seq & seq1 /" (- seq) = - (seq1 /" seq) )
thus - (seq1 /" seq) = (- 1) (#) (seq1 (#) (seq "))
.= (- seq1) /" seq by Th26 ; :: thesis: seq1 /" (- seq) = - (seq1 /" seq)
thus seq1 /" (- seq) = seq1 (#) ((- 1) (#) (seq ")) by Lm1, Th54
.= - (seq1 /" seq) by Th27 ; :: thesis: verum