let D be set ; :: thesis: for f being FinSequence holds
( f is D -valued iff f is FinSequence of D )
let f be FinSequence; :: thesis: ( f is D -valued iff f is FinSequence of D )
( f is D -valued implies f is FinSequence of D )

proof

assume f is D -valued ; :: thesis: f is FinSequence of D
then rng f c= D by RELAT_1:def 19;
hence f is FinSequence of D by FINSEQ_1:def 4; :: thesis: verum

end;

hence ( f is D -valued iff f is FinSequence of D ) ; :: thesis: verum