let 0L be lower-bounded Lattice; :: thesis: for f being Function of the carrier of 0L, the carrier of 0L holds FinJoin (({}. the carrier of 0L),f) = Bottom 0L
let f be Function of the carrier of 0L, the carrier of 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:40
.= Bottom 0L by LATTICE2:68 ; :: thesis: verum