:: deftheorem DefBaseFunc02 defines BaseFunc02 POSET_2:def 11 :
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:],Y
for x, y1, y2 being object holds
( ( x in D implies BaseFunc02 (x,y1,y2,I,J,D) = I . x ) & ( not x in D & x in X & y1 in Y & y2 in Y implies BaseFunc02 (x,y1,y2,I,J,D) = J . [x,y1,y2] ) & ( not x in D & ( x in D or not x in X or not y1 in Y or not y2 in Y ) implies BaseFunc02 (x,y1,y2,I,J,D) = Y ) );