let f be complex-valued XFinSequence; :: thesis: for x being Nat holds (Sequel f) . x = f . x
let x be Nat; :: thesis: (Sequel f) . x = f . x
x in NAT by ORDINAL1:def 12;
then A1: x in (dom (NAT --> 0)) \/ (dom f) by XBOOLE_0:def 3;

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

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

hence (Sequel f) . x = f . x by A1, FUNCT_4:def 1; :: thesis: verum

end;

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

then (Sequel f) . x = (NAT --> 0) . x by A1, FUNCT_4:def 1
.= 0 ;
hence (Sequel f) . x = f . x by B1, FUNCT_1:def 2; :: thesis: verum

end;

end;