let F be Function-yielding Function; :: thesis: ( F is Y -support-yielding implies F is X -support-yielding )
assume A1: F is Y -support-yielding ; :: thesis: F is X -support-yielding
let f be Function; :: according to MATRTOP3:def 1 :: thesis: for x being set st f in dom F & (F . f) . x <> f . x holds
x in X
let x be set ; :: thesis: ( f in dom F & (F . f) . x <> f . x implies x in X )
assume ( f in dom F & (F . f) . x <> f . x ) ; :: thesis: x in X
then x in Y by A1;
hence x in X ; :: thesis: verum