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

proof

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

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

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

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

end;

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

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

end;

end;

end;

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