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 Th15
.= (- seq1) /" seq ; :: thesis: seq1 /" (- seq) = - (seq1 /" seq)
thus seq1 /" (- seq) = seq1 (#) ((- 1r ) (#) (seq " )) by A1, Th44
.= (- 1r ) (#) (seq1 (#) (seq " )) by Th16
.= - (seq1 /" seq) ; :: thesis: verum