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_{1}( 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))))

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_{1}(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 ;

.= 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

let K be Element of Normal_forms_on A; :: thesis: FinJoin (K,(Atom A)) = FinUnion (K,(singleton (DISJOINT_PAIRS A)))

deffunc H

A1: FinUnion (K,(singleton (DISJOINT_PAIRS A))) c= mi (FinUnion (K,(singleton (DISJOINT_PAIRS A))))

proof

A10:
mi (FinUnion (K,(singleton (DISJOINT_PAIRS A)))) c= FinUnion (K,(singleton (DISJOINT_PAIRS A)))
by NORMFORM:40;
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;

end;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

hence
a in mi (FinUnion (K,(singleton (DISJOINT_PAIRS A))))
by A2, NORMFORM:39; :: thesis: verums = 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;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

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

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;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

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

thus FinJoin (K,(Atom A)) =
the L_join of (NormForm A) $$ (K,(Atom A))
by LATTICE2:def 3
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 (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

.= 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