let X be RealUnitarySpace; :: thesis: for seq1, seq2 being sequence of X
for k being Element of NAT holds (seq1 - seq2) ^\ k = (seq1 ^\ k) - (seq2 ^\ k)
let seq1, seq2 be sequence of X; :: thesis: for k being Element of NAT holds (seq1 - seq2) ^\ k = (seq1 ^\ k) - (seq2 ^\ k)
let k be Element of NAT ; :: thesis: (seq1 - seq2) ^\ k = (seq1 ^\ k) - (seq2 ^\ k)
thus (seq1 - seq2) ^\ k = (seq1 + (- seq2)) ^\ k by BHSP_1:71
.= (seq1 ^\ k) + ((- seq2) ^\ k) by Th38
.= (seq1 ^\ k) + (- (seq2 ^\ k)) by Th39
.= (seq1 ^\ k) - (seq2 ^\ k) by BHSP_1:71 ; :: thesis: verum