let f be complex-valued XFinSequence; :: thesis: Sum f = Sum (Sequel f)
reconsider g = Re (Sequel f) as real-valued Complex_Sequence ;
reconsider h = Im (Sequel f) as real-valued Complex_Sequence ;
A1: ( Sum (Re f) = Sum (Sequel (Re f)) & Sum (Im f) = Sum (Sequel (Im f)) ) by SSF;
A2: ( Sequel (Re f) = Re (Sequel f) & Sequel (Im f) = Im (Sequel f) ) by RSF, ISF;
Sum f = (Sum (Sequel (Re f))) + (<i> * (Sum (Sequel (Im f)))) by A1, RSI
.= (Sum g) + (Sum (<i> (#) h)) by A2, COMSEQ_3:56
.= Sum (g + (<i> (#) h)) by COMSEQ_3:54 ;
hence Sum f = Sum (Sequel f) ; :: thesis: verum