let k be Nat; :: thesis: for seq being Complex_Sequence holds (seq ") ^\ k = (seq ^\ k) "
let seq be Complex_Sequence; :: thesis: (seq ") ^\ k = (seq ^\ k) "

now :: thesis: for n being Element of NAT holds ((seq ") ^\ k) . n = ((seq ^\ k) ") . n

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

end;

hence (seq ") ^\ k = (seq ^\ k) " ; :: thesis: verum