let X be Function; :: thesis: ( X is empty implies X is XFinSequence-yielding )
assume A1: X is empty ; :: thesis: X is XFinSequence-yielding
let x be set ; :: according to REWRITE2:def 1 :: thesis: ( x in dom X implies X . x is XFinSequence )
thus ( x in dom X implies X . x is XFinSequence ) by A1; :: thesis: verum