:: Finite Join and Finite Meet, and Dual Lattices :: by Andrzej Trybulec :: :: Received August 10, 1990 :: Copyright (c) 1990-2012 Association of Mizar Users
for A being set for C being non emptyset for B being Subset of A for f, g being Function of A,C holds ( f | B = g | B iff for x being Element of A st x in B holds g . x = f . x )
for A being set for C being non emptyset for B being Subset of A for g, f being Function of A,C st ( for x being Element of A st x in B holds g . x = f . x ) holds f +*(g | B)= f