let A be set ; :: thesis: for K being Element of Normal_forms_on A holds FinJoin (K,(Atom A)) = FinUnion (K,())
let K be Element of Normal_forms_on A; :: thesis: FinJoin (K,(Atom A)) = FinUnion (K,())
deffunc H1( Element of Fin ()) -> Element of Normal_forms_on A = mi \$1;
A1: FinUnion (K,()) c= mi (FinUnion (K,()))
proof
let a be Element of DISJOINT_PAIRS A; :: according to HEYTING1:def 1 :: thesis: ( a in FinUnion (K,()) implies a in mi (FinUnion (K,())) )
assume A2: a in FinUnion (K,()) ; :: thesis: a in mi (FinUnion (K,()))
then consider b being Element of DISJOINT_PAIRS A such that
A3: b in K and
A4: a in () . b by SETWISEO:57;
A5: a = b by ;
now :: thesis: for s being Element of DISJOINT_PAIRS A st s in FinUnion (K,()) & s c= a holds
s = a
let s be Element of DISJOINT_PAIRS A; :: thesis: ( s in FinUnion (K,()) & s c= a implies s = a )
assume that
A6: s in FinUnion (K,()) 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 () . t by ;
s = t by ;
hence s = a by ; :: thesis: verum
end;
hence a in mi (FinUnion (K,())) by ; :: thesis: verum
end;
A10: mi (FinUnion (K,())) c= FinUnion (K,()) by NORMFORM:40;
consider g being Function of (),() such that
A11: for B being Element of Fin () holds g . B = H1(B) from reconsider g = g as Function of (), the carrier of () by NORMFORM:def 12;
A12: g . () = mi () by A11
.= {} by
.= Bottom () by NORMFORM:57
.= the_unity_wrt the L_join of () by LATTICE2:18 ;
A13: now :: thesis: for x, y being Element of Fin () holds g . (x \/ y) = the L_join of () . ((g . x),(g . y))
let x, y be Element of Fin (); :: thesis: g . (x \/ y) = the L_join of () . ((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 () . ((g . x),(g . y)) by ; :: thesis: verum
end;
A15: now :: thesis: for a being Element of DISJOINT_PAIRS A holds (g * ()) . a = (Atom A) . a
let a be Element of DISJOINT_PAIRS A; :: thesis: (g * ()) . a = (Atom A) . a
thus (g * ()) . a = g . (() . 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 () \$\$ (K,(Atom A)) by LATTICE2:def 3
.= the L_join of () \$\$ (K,(g * ())) by
.= g . (FinUnion (K,())) by
.= mi (FinUnion (K,())) by A11
.= FinUnion (K,()) by ; :: thesis: verum