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