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;
A1: ( the L_join of 0L is commutative & the L_join of 0L is associative ) by LATTICE2:27, LATTICE2:29;
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 A1, LATTICE2:67, SETWISEO:40
.= Bottom 0L by LATTICE2:68 ; :: thesis: verum