:: deftheorem DefFlatten01 defines Flatten POSET_2:def 4 :
for x being object
for X, Y being non empty set
for f being Function of X,Y holds
( ( x in X implies Flatten (f,x) = f . x ) & ( not x in X implies Flatten (f,x) = Y ) );