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

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

end;

{ (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

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 } )
consider f' being Element of Funcs (DISJOINT_PAIRS A),[:(Fin A),(Fin A):];
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) .: f',(incl (DISJOINT_PAIRS A))) by A5;
f' .: K c= L by 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 A6; :: thesis: verum

end;

end;

hence K =>> L = {[{} ,{} ]} by A1, ZFMISC_1:52; :: thesis: verum