theorem :: LATTICE2:35

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 "\/" (FinJoin (B,f)) = FinJoin (B,( the L_join of L [;] (v,f))) by Th20, SETWISEO:27;