let 1L be upper-bounded Lattice; :: thesis: for B being Element of Fin the carrier of 1L
for f, g being UnOp of the carrier of 1L holds FinMeet ((f .: B),g) = FinMeet (B,(g * f))
let B be Element of Fin the carrier of 1L; :: thesis: for f, g being UnOp of the carrier of 1L holds FinMeet ((f .: B),g) = FinMeet (B,(g * f))
let f, g be UnOp of the carrier of 1L; :: thesis: FinMeet ((f .: B),g) = FinMeet (B,(g * f))
set M = the L_meet of 1L;
thus FinMeet ((f .: B),g) = the L_meet of 1L $$ ((f .: B),g) by LATTICE2:def 4
.= the L_meet of 1L $$ (B,(g * f)) by SETWISEO:35
.= FinMeet (B,(g * f)) by LATTICE2:def 4 ; :: thesis: verum