let N be Element of NAT ; :: thesis: for seq1, seq2, seq3 being Real_Sequence of N holds seq1 - (seq2 - seq3) = (seq1 - seq2) + seq3
let seq1, seq2, seq3 be Real_Sequence of N; :: thesis: seq1 - (seq2 - seq3) = (seq1 - seq2) + seq3
thus seq1 - (seq2 - seq3) = seq1 + ((- 1) * (seq2 - seq3)) by Th12
.= seq1 + (((- 1) * seq2) - ((- 1) * seq3)) by Th15
.= seq1 + ((- seq2) - ((- 1) * seq3)) by Th12
.= seq1 + ((- seq2) - (- seq3)) by Th12
.= seq1 + ((- seq2) + seq3) by Th18
.= (seq1 - seq2) + seq3 by Th11 ; :: thesis: verum