:: deftheorem defines \+\ NORMFORM:def 5 :
for A, B being non empty preBoolean set
for x, y being Element of [:A,B:] holds x \+\ y = [((x `1) \+\ (y `1)),((x `2) \+\ (y `2))];