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 Def5
.= Re (((Partial_Sums seq) ^\ k) . n) by NAT_1:def 3
.= (Re ((Partial_Sums seq) ^\ k)) . n by Def5 ; :: 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 Def6
.= Im (((Partial_Sums seq) ^\ k) . n) by NAT_1:def 3
.= (Im ((Partial_Sums seq) ^\ k)) . n by Def6 ; :: thesis: verum