let f be complex-valued XFinSequence; :: thesis: Re (Sequel f) = Sequel (Re f)
dom (Sequel f) = NAT by COMSEQ_1:1;
then A2: dom (Re (Sequel f)) = NAT by COMSEQ_3:def 3;
for x being object st x in dom (Re (Sequel f)) holds
(Re (Sequel f)) . x = (Sequel (Re f)) . x

proof

let x be object ; :: thesis: ( x in dom (Re (Sequel f)) implies (Re (Sequel f)) . x = (Sequel (Re f)) . x )
assume B1: x in dom (Re (Sequel f)) ; :: thesis: (Re (Sequel f)) . x = (Sequel (Re f)) . x
then reconsider x = x as Nat ;
B2: (Re (Sequel f)) . x = Re ((Sequel f) . x) by B1, COMSEQ_3:def 3
.= Re (f . x) by SFX ;
B3: (Re f) . x = (Sequel (Re f)) . x by SFX;

per cases ( x in dom (Re f) or not x in dom (Re f) ) ;

suppose x in dom (Re f) ; :: thesis: (Re (Sequel f)) . x = (Sequel (Re f)) . x

hence (Re (Sequel f)) . x = (Sequel (Re f)) . x by B2, B3, COMSEQ_3:def 3; :: thesis: verum

end;

suppose not x in dom (Re f) ; :: thesis: (Re (Sequel f)) . x = (Sequel (Re f)) . x

then C1: ( (Re f) . x = 0 & not x in dom f ) by COMSEQ_3:def 3, FUNCT_1:def 2;
then f . x = 0 by FUNCT_1:def 2;
hence (Re (Sequel f)) . x = (Sequel (Re f)) . x by B2, SFX, C1; :: thesis: verum

end;

end;

end;

hence Re (Sequel f) = Sequel (Re f) by A2, COMSEQ_1:1; :: thesis: verum