let f be Function of [:NAT,NAT:],ExtREAL; :: thesis: ( lim_in_cod1 f = lim_in_cod2 (~ f) & lim_in_cod2 f = lim_in_cod1 (~ f) )

now :: thesis: for n being Element of NAT holds (lim_in_cod1 f) . n = (lim_in_cod2 (~ f)) . n

let n be Element of NAT ; :: thesis: (lim_in_cod1 f) . n = (lim_in_cod2 (~ f)) . n
(lim_in_cod1 f) . n = lim (ProjMap2 (f,n)) by D1DEF5
.= lim (ProjMap1 ((~ f),n)) by Th33 ;
hence (lim_in_cod1 f) . n = (lim_in_cod2 (~ f)) . n by D1DEF6; :: thesis: verum

end;

hence lim_in_cod1 f = lim_in_cod2 (~ f) by FUNCT_2:def 8; :: thesis: lim_in_cod2 f = lim_in_cod1 (~ f)

now :: thesis: for n being Element of NAT holds (lim_in_cod2 f) . n = (lim_in_cod1 (~ f)) . n

let n be Element of NAT ; :: thesis: (lim_in_cod2 f) . n = (lim_in_cod1 (~ f)) . n
(lim_in_cod2 f) . n = lim (ProjMap1 (f,n)) by D1DEF6
.= lim (ProjMap2 ((~ f),n)) by Th32 ;
hence (lim_in_cod2 f) . n = (lim_in_cod1 (~ f)) . n by D1DEF5; :: thesis: verum

end;

hence lim_in_cod2 f = lim_in_cod1 (~ f) by FUNCT_2:def 8; :: thesis: verum