let D1, D2 be set ; :: thesis: for f being Function holds
( f is Functional_Sequence of D1,D2 iff ( dom f = NAT & ( for x being set st x in NAT holds
f . x is PartFunc of D1,D2 ) ) )
let f be Function; :: thesis: ( f is Functional_Sequence of D1,D2 iff ( dom f = NAT & ( for x being set st x in NAT holds
f . x is PartFunc of D1,D2 ) ) )
thus ( f is Functional_Sequence of D1,D2 implies ( dom f = NAT & ( for x being set st x in NAT holds
f . x is PartFunc of D1,D2 ) ) ) :: thesis: ( dom f = NAT & ( for x being set st x in NAT holds
f . x is PartFunc of D1,D2 ) implies f is Functional_Sequence of D1,D2 )

proof

assume A1: f is Functional_Sequence of D1,D2 ; :: thesis: ( dom f = NAT & ( for x being set st x in NAT holds
f . x is PartFunc of D1,D2 ) )
hence dom f = NAT by FUNCT_2:def 1; :: thesis: for x being set st x in NAT holds
f . x is PartFunc of D1,D2
let x be set ; :: thesis: ( x in NAT implies f . x is PartFunc of D1,D2 )
assume x in NAT ; :: thesis: f . x is PartFunc of D1,D2
then x in dom f by A1, FUNCT_2:def 1;
then A2: f . x in rng f by FUNCT_1:def 5;
rng f c= PFuncs D1,D2 by A1, RELAT_1:def 19;
hence f . x is PartFunc of D1,D2 by A2, PARTFUN1:120; :: thesis: verum

end;

assume that
A3: dom f = NAT and
A4: for x being set st x in NAT holds
f . x is PartFunc of D1,D2 ; :: thesis: f is Functional_Sequence of D1,D2

now

let y be set ; :: thesis: ( y in rng f implies y in PFuncs D1,D2 )
assume y in rng f ; :: thesis: y in PFuncs D1,D2
then consider x being set such that
A5: x in dom f and
A6: y = f . x by FUNCT_1:def 5;
f . x is PartFunc of D1,D2 by A3, A4, A5;
hence y in PFuncs D1,D2 by A6, PARTFUN1:119; :: thesis: verum

end;

then rng f c= PFuncs D1,D2 by TARSKI:def 3;
hence f is Functional_Sequence of D1,D2 by A3, FUNCT_2:def 1, RELSET_1:11; :: thesis: verum