let D1, D2 be 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 ) ) )
let f be Function; ( f is Functional_Sequence of D1,D2 iff ( dom f = NAT & ( for n being Nat holds f . n is PartFunc of D1,D2 ) ) )
thus
( f is Functional_Sequence of D1,D2 implies ( dom f = NAT & ( for n being Nat holds f . n is PartFunc of D1,D2 ) ) )
by Lm1, ORDINAL1:def 12; ( dom f = NAT & ( for n being Nat holds f . n is PartFunc of D1,D2 ) implies f is Functional_Sequence of D1,D2 )
assume that
A1:
dom f = NAT
and
A2:
for n being Nat holds f . n is PartFunc of D1,D2
; f is Functional_Sequence of D1,D2
for x being set st x in NAT holds
f . x is PartFunc of D1,D2
by A2;
hence
f is Functional_Sequence of D1,D2
by A1, Lm1; verum