:: deftheorem defines ` GROUP_5:def 9 :
for G being Group holds G ` = [.((Omega). G),((Omega). G).];