let D1, D2 be set ; :: thesis: 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; :: thesis: ( 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum