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