let X be RealUnitarySpace; :: 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 BHSP_1:49
.= (seq1 ^\ k) + ((- seq2) ^\ k) by Th13
.= (seq1 ^\ k) + (- (seq2 ^\ k)) by Th14
.= (seq1 ^\ k) - (seq2 ^\ k) by BHSP_1:49 ; :: thesis: verum