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 )

( 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

hence
( f is D -valued iff f is FinSequence of D )
; :: thesis: verum
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;then rng f c= D by RELAT_1:def 19;

hence f is FinSequence of D by FINSEQ_1:def 4; :: thesis: verum