let X be ComplexUnitarySpace; :: thesis: for seq1, seq2 being sequence of X
for k being Nat holds (seq1 - seq2) ^\ k = (seq1 ^\ k) - (seq2 ^\ k)
let seq1, seq2 be sequence of X; :: thesis: for k being Nat holds (seq1 - seq2) ^\ k = (seq1 ^\ k) - (seq2 ^\ k)
let k be Nat; :: thesis: (seq1 - seq2) ^\ k = (seq1 ^\ k) - (seq2 ^\ k)
thus (seq1 - seq2) ^\ k = (seq1 + (- seq2)) ^\ k by CSSPACE:64
.= (seq1 ^\ k) + ((- seq2) ^\ k) by Th86
.= (seq1 ^\ k) + (- (seq2 ^\ k)) by Th87
.= (seq1 ^\ k) - (seq2 ^\ k) by CSSPACE:64 ; :: thesis: verum