let F be Function-yielding Function; :: thesis: ( F is X -support-yielding & F is Y -support-yielding implies F is X /\ Y -support-yielding )
assume A1: ( F is X -support-yielding & F is Y -support-yielding ) ; :: thesis: F is X /\ Y -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 /\ Y
let x be set ; :: thesis: ( f in dom F & (F . f) . x <> f . x implies x in X /\ Y )
assume ( f in dom F & (F . f) . x <> f . x ) ; :: thesis: x in X /\ Y
then ( x in X & x in Y ) by A1;
hence x in X /\ Y by XBOOLE_0:def 4; :: thesis: verum