let seq, seq1 be Complex_Sequence; :: thesis: ( seq is non-zero implies ( - (seq1 /" seq) = (- seq1) /" seq & seq1 /" (- seq) = - (seq1 /" seq) ) )
assume A1: seq is non-zero ; :: thesis: ( - (seq1 /" seq) = (- seq1) /" seq & seq1 /" (- seq) = - (seq1 /" seq) )
thus - (seq1 /" seq) = (- 1r) (#) (seq1 /" seq)
.= ((- 1r) (#) seq1) (#) (seq ") by Th12
.= (- seq1) /" seq ; :: thesis: seq1 /" (- seq) = - (seq1 /" seq)
thus seq1 /" (- seq) = seq1 (#) ((- 1r) (#) (seq ")) by A1, Th40
.= (- 1r) (#) (seq1 (#) (seq ")) by Th13
.= - (seq1 /" seq) ; :: thesis: verum