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 3;
rng f c= PFuncs (D1,D2) by A1, RELAT_1:def 19;
hence f . x is PartFunc of D1,D2 by A2, PARTFUN1:46; :: 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 :: thesis: for y being object st y in rng f holds
y in PFuncs (D1,D2)

let y be object ; :: 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 object such that
A5: x in dom f and
A6: y = f . x by FUNCT_1:def 3;
f . x is PartFunc of D1,D2 by A3, A4, A5;
hence y in PFuncs (D1,D2) by A6, PARTFUN1:45; :: thesis: verum

end;

then rng f c= PFuncs (D1,D2) ;
hence f is Functional_Sequence of D1,D2 by A3, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum