let A be set ; :: thesis: for B, C being Element of Fin (DISJOINT_PAIRS A)
for c being Element of DISJOINT_PAIRS A st c in B =>> C holds
ex f being Element of Funcs (DISJOINT_PAIRS A),[:(Fin A),(Fin A):] st
( f .: B c= C & c = FinPairUnion B,((pair_diff A) .: f,(incl (DISJOINT_PAIRS A))) )
let B, C be Element of Fin (DISJOINT_PAIRS A); :: thesis: for c being Element of DISJOINT_PAIRS A st c in B =>> C holds
ex f being Element of Funcs (DISJOINT_PAIRS A),[:(Fin A),(Fin A):] st
( f .: B c= C & c = FinPairUnion B,((pair_diff A) .: f,(incl (DISJOINT_PAIRS A))) )
let c be Element of DISJOINT_PAIRS A; :: thesis: ( c in B =>> C implies ex f being Element of Funcs (DISJOINT_PAIRS A),[:(Fin A),(Fin A):] st
( f .: B c= C & c = FinPairUnion B,((pair_diff A) .: f,(incl (DISJOINT_PAIRS A))) ) )
assume c in B =>> C ; :: thesis: ex f being Element of Funcs (DISJOINT_PAIRS A),[:(Fin A),(Fin A):] st
( f .: B c= C & c = FinPairUnion B,((pair_diff A) .: f,(incl (DISJOINT_PAIRS A))) )
then c in { (FinPairUnion B,((pair_diff A) .: f,(incl (DISJOINT_PAIRS A)))) where f is Element of Funcs (DISJOINT_PAIRS A),[:(Fin A),(Fin A):] : f .: B c= C } by XBOOLE_0:def 4;
then ex f being Element of Funcs (DISJOINT_PAIRS A),[:(Fin A),(Fin A):] st
( c = FinPairUnion B,((pair_diff A) .: f,(incl (DISJOINT_PAIRS A))) & f .: B c= C ) ;
hence ex f being Element of Funcs (DISJOINT_PAIRS A),[:(Fin A),(Fin A):] st
( f .: B c= C & c = FinPairUnion B,((pair_diff A) .: f,(incl (DISJOINT_PAIRS A))) ) ; :: thesis: verum