let A be set ; :: thesis: for K being Element of Normal_forms_on A holds FinJoin K,(Atom A) = FinUnion K,(singleton (DISJOINT_PAIRS A))
let K be Element of Normal_forms_on A; :: thesis: FinJoin K,(Atom A) = FinUnion K,(singleton (DISJOINT_PAIRS A))
A1: ( the L_join of (NormForm A) is commutative & the L_join of (NormForm A) is associative ) by LATTICE2:27, LATTICE2:29;
deffunc H₁( Element of Fin (DISJOINT_PAIRS A)) -> Element of Normal_forms_on A = mi $1;
A2: the L_join of (NormForm A) is idempotent by LATTICE2:26;
A3: FinUnion K,(singleton (DISJOINT_PAIRS A)) c= mi (FinUnion K,(singleton (DISJOINT_PAIRS A)))

proof

let a be Element of DISJOINT_PAIRS A; :: according to HEYTING1:def 1 :: thesis: ( a in FinUnion K,(singleton (DISJOINT_PAIRS A)) implies a in mi (FinUnion K,(singleton (DISJOINT_PAIRS A))) )
assume A4: a in FinUnion K,(singleton (DISJOINT_PAIRS A)) ; :: thesis: a in mi (FinUnion K,(singleton (DISJOINT_PAIRS A)))
then consider b being Element of DISJOINT_PAIRS A such that
A5: b in K and
A6: a in (singleton (DISJOINT_PAIRS A)) . b by SETWISEO:70;
A7: a = b by A6, SETWISEO:68;

now

let s be Element of DISJOINT_PAIRS A; :: thesis: ( s in FinUnion K,(singleton (DISJOINT_PAIRS A)) & s c= a implies s = a )
assume that
A8: s in FinUnion K,(singleton (DISJOINT_PAIRS A)) and
A9: s c= a ; :: thesis: s = a
consider t being Element of DISJOINT_PAIRS A such that
A10: t in K and
A11: s in (singleton (DISJOINT_PAIRS A)) . t by A8, SETWISEO:70;
s = t by A11, SETWISEO:68;
hence s = a by A5, A7, A9, A10, NORMFORM:52; :: thesis: verum

end;

hence a in mi (FinUnion K,(singleton (DISJOINT_PAIRS A))) by A4, NORMFORM:61; :: thesis: verum

end;

A12: mi (FinUnion K,(singleton (DISJOINT_PAIRS A))) c= FinUnion K,(singleton (DISJOINT_PAIRS A)) by NORMFORM:64;
consider g being Function of (Fin (DISJOINT_PAIRS A)),(Normal_forms_on A) such that
A13: for B being Element of Fin (DISJOINT_PAIRS A) holds g . B = H₁(B) from FUNCT_2:sch 4();
reconsider g = g as Function of (Fin (DISJOINT_PAIRS A)),the carrier of (NormForm A) by NORMFORM:def 14;
A14: g . ({}. (DISJOINT_PAIRS A)) = mi ({}. (DISJOINT_PAIRS A)) by A13
.= {} by NORMFORM:64, XBOOLE_1:3
.= Bottom (NormForm A) by NORMFORM:86
.= the_unity_wrt the L_join of (NormForm A) by LATTICE2:28, LATTICE2:67 ;

A15: now

let x, y be Element of Fin (DISJOINT_PAIRS A); :: thesis: g . (x \/ y) = the L_join of (NormForm A) . (g . x),(g . y)
A16: ( @ (g . x) = mi x & @ (g . y) = mi y ) by A13;
thus g . (x \/ y) = mi (x \/ y) by A13
.= mi ((mi x) \/ y) by NORMFORM:68
.= mi ((mi x) \/ (mi y)) by NORMFORM:69
.= the L_join of (NormForm A) . (g . x),(g . y) by A16, NORMFORM:def 14 ; :: thesis: verum

end;

A17: now

let a be Element of DISJOINT_PAIRS A; :: thesis: (g * (singleton (DISJOINT_PAIRS A))) . a = (Atom A) . a
thus (g * (singleton (DISJOINT_PAIRS A))) . a = g . ((singleton (DISJOINT_PAIRS A)) . a) by FUNCT_2:21
.= g . {a} by SETWISEO:67
.= mi {a} by A13
.= {a} by NORMFORM:66
.= (Atom A) . a by Def4 ; :: thesis: verum

end;

thus FinJoin K,(Atom A) = the L_join of (NormForm A) $$ K,(Atom A) by LATTICE2:def 3
.= the L_join of (NormForm A) $$ K,(g * (singleton (DISJOINT_PAIRS A))) by A17, FUNCT_2:113
.= g . (FinUnion K,(singleton (DISJOINT_PAIRS A))) by A1, A2, A14, A15, LATTICE2:67, SETWISEO:65
.= mi (FinUnion K,(singleton (DISJOINT_PAIRS A))) by A13
.= FinUnion K,(singleton (DISJOINT_PAIRS A)) by A12, A3, XBOOLE_0:def 10 ; :: thesis: verum