let A be set ; 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); 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; ( 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
; 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))))) )
; verum