:: deftheorem Def61 defines RVswitchsecond FINANCE6:def 21 :
for n being Nat holds
( ( n = 1 implies RVswitchsecond n = RVfirst 5 ) & ( not n = 1 implies RVswitchsecond n = RVfirst 0 ) );