let F be Function; :: thesis: ( F is empty implies F is FinSequence-yielding )
assume Z: F is empty ; :: thesis: F is FinSequence-yielding
let x be set ; :: according to MATRLIN:def 1 :: thesis: ( not x in dom F or F . x is set )
thus ( not x in dom F or F . x is set ) by Z; :: thesis: verum