let f be Function; :: thesis: ( f = M /. k implies ( f is FinSequence-like & f is D -valued ) )
assume Z: f = M /. k ; :: thesis: ( f is FinSequence-like & f is D -valued )
B: f is Element of D * by Z;
then f is FinSequence of D by FINSEQ_1:def 11;
then C: f is D -valued ;
f is FinSequence-like by B;
hence ( f is FinSequence-like & f is D -valued ) by C; :: thesis: verum