:: deftheorem defines FinJoin LATTICE2:def 3 :
for A being non empty set
for L being Lattice
for B being Element of Fin A
for f being Function of A, the carrier of L holds FinJoin (B,f) = the L_join of L $$ (B,f);