let k be Element of NAT ; :: thesis: for seq, seq1 being Real_Sequence holds (seq - seq1) ^\ k = (seq ^\ k) - (seq1 ^\ k)
let seq, seq1 be Real_Sequence; :: thesis: (seq - seq1) ^\ k = (seq ^\ k) - (seq1 ^\ k)
thus (seq - seq1) ^\ k = (seq ^\ k) + ((- seq1) ^\ k) by Th37
.= (seq ^\ k) - (seq1 ^\ k) by Th38 ; :: thesis: verum