let A be non empty set ; :: thesis: for B being Finite_Subset of A
for L being D0_Lattice
for f being Function of A,the carrier of L
for u being Element of L holds the L_meet of L . u,(FinJoin B,f) = FinJoin B,(the L_meet of L [;] u,f)
let B be Finite_Subset of A; :: thesis: for L being D0_Lattice
for f being Function of A,the carrier of L
for u being Element of L holds the L_meet of L . u,(FinJoin B,f) = FinJoin B,(the L_meet of L [;] u,f)
let L be D0_Lattice; :: thesis: for f being Function of A,the carrier of L
for u being Element of L holds the L_meet of L . u,(FinJoin B,f) = FinJoin B,(the L_meet of L [;] u,f)
let f be Function of A,the carrier of L; :: thesis: for u being Element of L holds the L_meet of L . u,(FinJoin B,f) = FinJoin B,(the L_meet of L [;] u,f)
let u be Element of L; :: thesis: the L_meet of L . u,(FinJoin B,f) = FinJoin B,(the L_meet of L [;] u,f)
A1: ( the L_join of L is commutative & the L_join of L is associative & the L_meet of L is_distributive_wrt the L_join of L & the L_join of L is having_a_unity & Bottom L = the_unity_wrt the L_join of L ) by Th37, Th67, Th68;
the L_meet of L . u,(Bottom L) = u "/\" (Bottom L)
.= Bottom L by LATTICES:40 ;
hence the L_meet of L . u,(FinJoin B,f) = FinJoin B,(the L_meet of L [;] u,f) by A1, SETWOP_2:14; :: thesis: verum