:: deftheorem defines ?. PRALG_2:def 12 :
for I being set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S holds A ?. o = (commute (OPER A)) . o;