let k be Element of NAT ; :: thesis: for seq, seq1 being Complex_Sequence holds (seq - seq1) ^\ k = (seq ^\ k) - (seq1 ^\ k)
let seq, seq1 be Complex_Sequence; :: thesis: (seq - seq1) ^\ k = (seq ^\ k) - (seq1 ^\ k)

now

let n be Element of NAT ; :: thesis: ((seq - seq1) ^\ k) . n = ((seq ^\ k) - (seq1 ^\ k)) . n
thus ((seq - seq1) ^\ k) . n = (seq + (- seq1)) . (n + k) by NAT_1:def 3
.= (seq . (n + k)) + ((- seq1) . (n + k)) by VALUED_1:1
.= (seq . (n + k)) + (- (seq1 . (n + k))) by VALUED_1:8
.= ((seq ^\ k) . n) - (seq1 . (n + k)) by NAT_1:def 3
.= ((seq ^\ k) . n) + (- ((seq1 ^\ k) . n)) by NAT_1:def 3
.= ((seq ^\ k) . n) + ((- (seq1 ^\ k)) . n) by VALUED_1:8
.= ((seq ^\ k) - (seq1 ^\ k)) . n by VALUED_1:1 ; :: thesis: verum

end;

hence (seq - seq1) ^\ k = (seq ^\ k) - (seq1 ^\ k) by FUNCT_2:113; :: thesis: verum