:: deftheorem Def5 defines Effect_IPC INTPRO_2:def 5 :
for f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st f <> {} holds
Effect_IPC f = (f . (len f)) `1 ;