let A be set ; :: thesis: for K, L being Element of Normal_forms_on A st K = {} & L = {} holds
K =>> L = {[{},{}]}
let K, L be Element of Normal_forms_on A; :: thesis: ( K = {} & L = {} implies K =>> L = {[{},{}]} )
assume that
A1: K = {} and
L = {} ; :: thesis: K =>> L = {[{},{}]}
A2: {} = {}. A ;
A3: K = {}. (DISJOINT_PAIRS A) by A1;
A4: now :: thesis: for f being Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) holds FinPairUnion (K,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A))))) = [{},{}]
let f be Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]); :: thesis: FinPairUnion (K,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A))))) = [{},{}]
thus FinPairUnion (K,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A))))) = the_unity_wrt (FinPairUnion A) by A3, NORMFORM:18, SETWISEO:31
.= [{},{}] by A2, NORMFORM:19 ; :: thesis: verum
end;
A5: { (FinPairUnion (K,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))))) where f is Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : f .: K c= L } = {[{},{}]}
proof
thus { (FinPairUnion (K,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))))) where f is Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : f .: K c= L } c= {[{},{}]} :: according to XBOOLE_0:def 10 :: thesis: {[{},{}]} c= { (FinPairUnion (K,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))))) where f is Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : f .: K c= L }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (FinPairUnion (K,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))))) where f is Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : f .: K c= L } or x in {[{},{}]} )
assume x in { (FinPairUnion (K,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))))) where f is Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : f .: K c= L } ; :: thesis: x in {[{},{}]}
then ex f being Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) st
( x = FinPairUnion (K,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A))))) & f .: K c= L ) ;
then x = [{},{}] by A4;
hence x in {[{},{}]} by TARSKI:def 1; :: thesis: verum
end;
thus {[{},{}]} c= { (FinPairUnion (K,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))))) where f is Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : f .: K c= L } :: thesis: verum
proof
set f9 = the Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]);
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {[{},{}]} or x in { (FinPairUnion (K,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))))) where f is Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : f .: K c= L } )
assume x in {[{},{}]} ; :: thesis: x in { (FinPairUnion (K,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))))) where f is Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : f .: K c= L }
then x = [{},{}] by TARSKI:def 1;
then A6: x = FinPairUnion (K,((pair_diff A) .: ( the Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]),(incl (DISJOINT_PAIRS A))))) by A4;
the Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) .: K c= L by A1;
hence x in { (FinPairUnion (K,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))))) where f is Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : f .: K c= L } by A6; :: thesis: verum
end;
end;
[{},{}] is Element of DISJOINT_PAIRS A by Th12;
hence K =>> L = {[{},{}]} by A5, ZFMISC_1:46; :: thesis: verum