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

now

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) " by FUNCT_2:113; :: thesis: verum