:: deftheorem defines rseq BASEL_1:def 2 :
for a, b, c, d being Real holds rseq (a,b,c,d) = Re (Rat_Exp_Seq (a,b,c,d));