:: deftheorem DefFlatten04 defines Flatten POSET_2:def 5 :
for X, Y being non empty set
for f being Function of X,Y
for b₄ being Function of (FlatPoset X),(FlatPoset Y) holds
( b₄ = Flatten f iff ( b₄ . X = Y & ( for x being Element of (FlatPoset X) st x <> X holds
b₄ . x = f . x ) ) );