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

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