theorem Th38: :: DBLSEQ_3:38

for f being Function of [:NAT,NAT:],ExtREAL holds
( lim_in_cod1 f = lim_in_cod2 (~ f) & lim_in_cod2 f = lim_in_cod1 (~ f) )