let A be set ; :: thesis: for B being Element of Fin (DISJOINT_PAIRS A)

for c being Element of DISJOINT_PAIRS A st c in - B holds

ex g being Element of Funcs ((DISJOINT_PAIRS A),[A]) st

( ( for s being Element of DISJOINT_PAIRS A st s in B holds

g . s in (s `1) \/ (s `2) ) & c = [ { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in B ) } , { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in B ) } ] )

let B be Element of Fin (DISJOINT_PAIRS A); :: thesis: for c being Element of DISJOINT_PAIRS A st c in - B holds

ex g being Element of Funcs ((DISJOINT_PAIRS A),[A]) st

( ( for s being Element of DISJOINT_PAIRS A st s in B holds

g . s in (s `1) \/ (s `2) ) & c = [ { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in B ) } , { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in B ) } ] )

let c be Element of DISJOINT_PAIRS A; :: thesis: ( c in - B implies ex g being Element of Funcs ((DISJOINT_PAIRS A),[A]) st

( ( for s being Element of DISJOINT_PAIRS A st s in B holds

g . s in (s `1) \/ (s `2) ) & c = [ { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in B ) } , { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in B ) } ] ) )

assume c in - B ; :: thesis: ex g being Element of Funcs ((DISJOINT_PAIRS A),[A]) st

( ( for s being Element of DISJOINT_PAIRS A st s in B holds

g . s in (s `1) \/ (s `2) ) & c = [ { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in B ) } , { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in B ) } ] )

then c in { [ { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in B ) } , { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in B ) } ] where g is Element of Funcs ((DISJOINT_PAIRS A),[A]) : for s being Element of DISJOINT_PAIRS A st s in B holds

g . s in (s `1) \/ (s `2) } by XBOOLE_0:def 4;

then ex g being Element of Funcs ((DISJOINT_PAIRS A),[A]) st

( c = [ { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in B ) } , { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in B ) } ] & ( for s being Element of DISJOINT_PAIRS A st s in B holds

g . s in (s `1) \/ (s `2) ) ) ;

hence ex g being Element of Funcs ((DISJOINT_PAIRS A),[A]) st

( ( for s being Element of DISJOINT_PAIRS A st s in B holds

g . s in (s `1) \/ (s `2) ) & c = [ { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in B ) } , { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in B ) } ] ) ; :: thesis: verum

for c being Element of DISJOINT_PAIRS A st c in - B holds

ex g being Element of Funcs ((DISJOINT_PAIRS A),[A]) st

( ( for s being Element of DISJOINT_PAIRS A st s in B holds

g . s in (s `1) \/ (s `2) ) & c = [ { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in B ) } , { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in B ) } ] )

let B be Element of Fin (DISJOINT_PAIRS A); :: thesis: for c being Element of DISJOINT_PAIRS A st c in - B holds

ex g being Element of Funcs ((DISJOINT_PAIRS A),[A]) st

( ( for s being Element of DISJOINT_PAIRS A st s in B holds

g . s in (s `1) \/ (s `2) ) & c = [ { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in B ) } , { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in B ) } ] )

let c be Element of DISJOINT_PAIRS A; :: thesis: ( c in - B implies ex g being Element of Funcs ((DISJOINT_PAIRS A),[A]) st

( ( for s being Element of DISJOINT_PAIRS A st s in B holds

g . s in (s `1) \/ (s `2) ) & c = [ { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in B ) } , { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in B ) } ] ) )

assume c in - B ; :: thesis: ex g being Element of Funcs ((DISJOINT_PAIRS A),[A]) st

( ( for s being Element of DISJOINT_PAIRS A st s in B holds

g . s in (s `1) \/ (s `2) ) & c = [ { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in B ) } , { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in B ) } ] )

then c in { [ { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in B ) } , { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in B ) } ] where g is Element of Funcs ((DISJOINT_PAIRS A),[A]) : for s being Element of DISJOINT_PAIRS A st s in B holds

g . s in (s `1) \/ (s `2) } by XBOOLE_0:def 4;

then ex g being Element of Funcs ((DISJOINT_PAIRS A),[A]) st

( c = [ { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in B ) } , { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in B ) } ] & ( for s being Element of DISJOINT_PAIRS A st s in B holds

g . s in (s `1) \/ (s `2) ) ) ;

hence ex g being Element of Funcs ((DISJOINT_PAIRS A),[A]) st

( ( for s being Element of DISJOINT_PAIRS A st s in B holds

g . s in (s `1) \/ (s `2) ) & c = [ { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in B ) } , { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in B ) } ] ) ; :: thesis: verum