theorem :: SEQFUNC:1

for D1, D2 being set
for f being Function holds
( f is Functional_Sequence of D1,D2 iff ( dom f = NAT & ( for n being Nat holds f . n is PartFunc of D1,D2 ) ) )