let Y be set ; :: thesis: for g being Function st g is Y -valued & g is FinSequence-like holds
g is FinSequence of Y
let g be Function; :: thesis: ( g is Y -valued & g is FinSequence-like implies g is FinSequence of Y )
set f = g;
set X = Y;
assume B0: ( g is Y -valued & g is FinSequence-like ) ; :: thesis: g is FinSequence of Y
then reconsider p = g as FinSequence ;
rng p c= Y by B0, RELAT_1:def 19;
hence g is FinSequence of Y by FINSEQ_1:def 4; :: thesis: verum