let seq1, seq2 be Complex_Sequence; :: thesis: ( (- seq1) (#) seq2 = - (seq1 (#) seq2) & seq1 (#) (- seq2) = - (seq1 (#) seq2) )
thus (- seq1) (#) seq2 = ((- 1r ) (#) seq1) (#) seq2
.= (- 1r ) (#) (seq1 (#) seq2) by Th15
.= - (seq1 (#) seq2) ; :: thesis: seq1 (#) (- seq2) = - (seq1 (#) seq2)
thus seq1 (#) (- seq2) = seq1 (#) ((- 1r ) (#) seq2)
.= (- 1r ) (#) (seq1 (#) seq2) by Th16
.= - (seq1 (#) seq2) ; :: thesis: verum