for A being non empty set
for B being Element of Fin A
for L being D0_Lattice
for f, g being Function of A, the carrier of L
for u being Element of L st ( for x being Element of A st x in B holds
g . x = u "/\" (f . x) ) holds
u "/\" (FinJoin (B,f)) = FinJoin (B,g)