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)))
deffunc H₁( Element of Fin (DISJOINT_PAIRS A)) -> Element of Normal_forms_on A = mi $1;
A1: 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 A2: 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
A3: b in K and
A4: a in (singleton (DISJOINT_PAIRS A)) . b by SETWISEO:57;
A5: a = b by A4, SETWISEO:55;

now :: thesis: for s being Element of DISJOINT_PAIRS A st s in FinUnion (K,(singleton (DISJOINT_PAIRS A))) & s c= a holds
s = a

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
A6: s in FinUnion (K,(singleton (DISJOINT_PAIRS A))) and
A7: s c= a ; :: thesis: s = a
consider t being Element of DISJOINT_PAIRS A such that
A8: t in K and
A9: s in (singleton (DISJOINT_PAIRS A)) . t by A6, SETWISEO:57;
s = t by A9, SETWISEO:55;
hence s = a by A3, A5, A7, A8, NORMFORM:32; :: thesis: verum

end;

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

end;

A10: mi (FinUnion (K,(singleton (DISJOINT_PAIRS A)))) c= FinUnion (K,(singleton (DISJOINT_PAIRS A))) by NORMFORM:40;
consider g being Function of (Fin (DISJOINT_PAIRS A)),(Normal_forms_on A) such that
A11: 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 12;
A12: g . ({}. (DISJOINT_PAIRS A)) = mi ({}. (DISJOINT_PAIRS A)) by A11
.= {} by NORMFORM:40, XBOOLE_1:3
.= Bottom (NormForm A) by NORMFORM:57
.= the_unity_wrt the L_join of (NormForm A) by LATTICE2:18 ;

A13: now :: thesis: for x, y being Element of Fin (DISJOINT_PAIRS A) holds g . (x \/ y) = the L_join of (NormForm A) . ((g . x),(g . y))

let x, y be Element of Fin (DISJOINT_PAIRS A); :: thesis: g . (x \/ y) = the L_join of (NormForm A) . ((g . x),(g . y))
A14: ( @ (g . x) = mi x & @ (g . y) = mi y ) by A11;
thus g . (x \/ y) = mi (x \/ y) by A11
.= mi ((mi x) \/ y) by NORMFORM:44
.= mi ((mi x) \/ (mi y)) by NORMFORM:45
.= the L_join of (NormForm A) . ((g . x),(g . y)) by A14, NORMFORM:def 12 ; :: thesis: verum

end;

A15: now :: thesis: for a being Element of DISJOINT_PAIRS A holds (g * (singleton (DISJOINT_PAIRS A))) . a = (Atom A) . a

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:15
.= g . {a} by SETWISEO:54
.= mi {a} by A11
.= {a} by NORMFORM:42
.= (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 A15, FUNCT_2:63
.= g . (FinUnion (K,(singleton (DISJOINT_PAIRS A)))) by A12, A13, SETWISEO:53
.= mi (FinUnion (K,(singleton (DISJOINT_PAIRS A)))) by A11
.= FinUnion (K,(singleton (DISJOINT_PAIRS A))) by A10, A1 ; :: thesis: verum