let X be set ; :: thesis: ( X is FinSequence-membered implies X is functional )
assume Z: X is FinSequence-membered ; :: thesis: X is functional
let x be set ; :: according to FUNCT_1:def 19 :: thesis: ( not x in X or x is set )
assume x in X ; :: thesis: x is set
then x is FinSequence by Z, Def19;
hence x is Function ; :: thesis: verum