theorem :: LATTICE2:43

for L being Lattice
for v being Element of L
for A being non empty set
for B being Element of Fin A
for f being Function of A, the carrier of L st B <> {} holds
v "/\" (FinMeet (B,f)) = FinMeet (B,( the L_meet of L [;] (v,f))) by Th25, SETWISEO:27;