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

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