:: deftheorem Def2 defines /\/ STACKS_1:def 2 :
for C, D being non empty set
for R being Equivalence_Relation of D
for b being Function of [:C,D:],D st b is BinOp of C,D,R holds
for b₅ being Function of [:C,(Class R):],(Class R) holds
( b₅ = b /\/ R iff for x, y, y1 being set st x in C & y in Class R & y1 in y holds
b₅ . (x,y) = Class (R,(b . (x,y1))) );