:: deftheorem Def8 defines Set1_of_SigmaField3 FINANCE3:def 11 :
for k being Element of {1,2,3} holds
( ( k = 1 implies Set1_of_SigmaField3 k = Special_SigmaField1 ) & ( not k = 1 implies Set1_of_SigmaField3 k = Special_SigmaField2 ) );