let seq be Complex_Sequence; :: thesis: for k being Element of NAT holds
( (Partial_Sums (Re seq)) ^\ k = Re ((Partial_Sums seq) ^\ k) & (Partial_Sums (Im seq)) ^\ k = Im ((Partial_Sums seq) ^\ k) )
let k be Element of NAT ; :: thesis: ( (Partial_Sums (Re seq)) ^\ k = Re ((Partial_Sums seq) ^\ k) & (Partial_Sums (Im seq)) ^\ k = Im ((Partial_Sums seq) ^\ k) )

now

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

end;

hence ( (Partial_Sums (Re seq)) ^\ k = Re ((Partial_Sums seq) ^\ k) & (Partial_Sums (Im seq)) ^\ k = Im ((Partial_Sums seq) ^\ k) ) by FUNCT_2:113; :: thesis: verum