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

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

let n be Element of NAT ; :: thesis: ( ((Re seq) ^\ k) . n = (Re (seq ^\ k)) . n & ((Im seq) ^\ k) . n = (Im (seq ^\ k)) . n )
thus ((Re seq) ^\ k) . n = (Re seq) . (n + k) by NAT_1:def 3
.= Re (seq . (n + k)) by Def5
.= Re ((seq ^\ k) . n) by NAT_1:def 3
.= (Re (seq ^\ k)) . n by Def5 ; :: thesis: ((Im seq) ^\ k) . n = (Im (seq ^\ k)) . n
thus ((Im seq) ^\ k) . n = (Im seq) . (n + k) by NAT_1:def 3
.= Im (seq . (n + k)) by Def6
.= Im ((seq ^\ k) . n) by NAT_1:def 3
.= (Im (seq ^\ k)) . n by Def6 ; :: thesis: verum

end;

hence ( (Re seq) ^\ k = Re (seq ^\ k) & (Im seq) ^\ k = Im (seq ^\ k) ) ; :: thesis: verum