:: deftheorem DefBaseFunc01 defines BaseFunc01 POSET_2:def 8 :
for X, Y being non empty set
for D being Subset of X
for I being Function of X,Y
for J being Function of [:X,Y:],Y
for x, y being object holds
( ( x in D implies BaseFunc01 (x,y,I,J,D) = I . x ) & ( not x in D & x in X & y in Y implies BaseFunc01 (x,y,I,J,D) = J . [x,y] ) & ( not x in D & ( x in D or not x in X or not y in Y ) implies BaseFunc01 (x,y,I,J,D) = Y ) );