let 0L be lower-bounded Lattice; :: thesis: for f being Function of 0L,0L holds FinJoin (({}. the carrier of 0L),f) = Bottom 0L

let f be Function of 0L,0L; :: thesis: FinJoin (({}. the carrier of 0L),f) = Bottom 0L

set J = the L_join of 0L;

thus FinJoin (({}. the carrier of 0L),f) = the L_join of 0L $$ (({}. the carrier of 0L),f) by LATTICE2:def 3

.= the_unity_wrt the L_join of 0L by SETWISEO:31

.= Bottom 0L by LATTICE2:52 ; :: thesis: verum

let f be Function of 0L,0L; :: thesis: FinJoin (({}. the carrier of 0L),f) = Bottom 0L

set J = the L_join of 0L;

thus FinJoin (({}. the carrier of 0L),f) = the L_join of 0L $$ (({}. the carrier of 0L),f) by LATTICE2:def 3

.= the_unity_wrt the L_join of 0L by SETWISEO:31

.= Bottom 0L by LATTICE2:52 ; :: thesis: verum