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
A2: L = {} ; :: thesis: K =>> L = {[{} ,{} ]}
A3: {} = {}. A ;
A4: K = {}. (DISJOINT_PAIRS A) by A1;

A5: now

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 A4, NORMFORM:37, SETWISEO:40
.= [{} ,{} ] by A3, NORMFORM:38 ; :: thesis: verum

end;

A6: { (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 set ; :: 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 A5;
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

consider f9 being Element of Funcs (DISJOINT_PAIRS A),[:(Fin A),(Fin A):];
let x be set ; :: 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 A7: x = FinPairUnion K,((pair_diff A) .: f9,(incl (DISJOINT_PAIRS A))) by A5;
f9 .: K c= L by A1, A2, RELAT_1:149;
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 A7; :: thesis: verum

end;

end;

[{} ,{} ] is Element of DISJOINT_PAIRS A by Th17;
hence K =>> L = {[{} ,{} ]} by A6, ZFMISC_1:52; :: thesis: verum