include('Axioms/real_topology_2.ax').
tff(tp_c_2Elebesgue_2ERADON__F,type,(c_2Elebesgue_2ERADON__F:del > $i)).
tff(mem_c_2Elebesgue_2ERADON__F,axiom,( ! [A_27a:del] : mem(c_2Elebesgue_2ERADON__F(A_27a),arr(ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),arr(ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),arr(arr(A_27a,ty_2Eextreal_2Eextreal),bool)))))).
tff(tp_c_2Elebesgue_2ERADON__F__integrals,type,(c_2Elebesgue_2ERADON__F__integrals:del > $i)).
tff(mem_c_2Elebesgue_2ERADON__F__integrals,axiom,( ! [A_27a:del] : mem(c_2Elebesgue_2ERADON__F__integrals(A_27a),arr(ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),arr(ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),arr(ty_2Eextreal_2Eextreal,bool)))))).
tff(tp_c_2Elebesgue_2Efinite__space__integral,type,(c_2Elebesgue_2Efinite__space__integral:del > $i)).
tff(mem_c_2Elebesgue_2Efinite__space__integral,axiom,( ! [A_27a:del] : mem(c_2Elebesgue_2Efinite__space__integral(A_27a),arr(ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),arr(arr(A_27a,ty_2Eextreal_2Eextreal),ty_2Eextreal_2Eextreal))))).
tff(tp_c_2Elebesgue_2Efn__seq,type,(c_2Elebesgue_2Efn__seq:del > $i)).
tff(mem_c_2Elebesgue_2Efn__seq,axiom,( ! [A_27a:del] : mem(c_2Elebesgue_2Efn__seq(A_27a),arr(ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),arr(arr(A_27a,ty_2Eextreal_2Eextreal),arr(ty_2Enum_2Enum,arr(A_27a,ty_2Eextreal_2Eextreal))))))).
tff(tp_c_2Elebesgue_2Efn__seq__integral,type,(c_2Elebesgue_2Efn__seq__integral:del > $i)).
tff(mem_c_2Elebesgue_2Efn__seq__integral,axiom,( ! [A_27a:del] : mem(c_2Elebesgue_2Efn__seq__integral(A_27a),arr(ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),arr(arr(A_27a,ty_2Eextreal_2Eextreal),arr(ty_2Enum_2Enum,ty_2Eextreal_2Eextreal)))))).
tff(tp_c_2Elebesgue_2Eintegrable,type,(c_2Elebesgue_2Eintegrable:del > $i)).
tff(mem_c_2Elebesgue_2Eintegrable,axiom,( ! [A_27a:del] : mem(c_2Elebesgue_2Eintegrable(A_27a),arr(ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),arr(arr(A_27a,ty_2Eextreal_2Eextreal),bool))))).
tff(tp_c_2Elebesgue_2Eintegral,type,(c_2Elebesgue_2Eintegral:del > $i)).
tff(mem_c_2Elebesgue_2Eintegral,axiom,( ! [A_27a:del] : mem(c_2Elebesgue_2Eintegral(A_27a),arr(ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),arr(arr(A_27a,ty_2Eextreal_2Eextreal),ty_2Eextreal_2Eextreal))))).
tff(tp_c_2Elebesgue_2Emax__fn__seq,type,(c_2Elebesgue_2Emax__fn__seq:del > $i)).
tff(mem_c_2Elebesgue_2Emax__fn__seq,axiom,( ! [A_27a:del] : mem(c_2Elebesgue_2Emax__fn__seq(A_27a),arr(arr(ty_2Enum_2Enum,arr(A_27a,ty_2Eextreal_2Eextreal)),arr(ty_2Enum_2Enum,arr(A_27a,ty_2Eextreal_2Eextreal)))))).
tff(tp_c_2Elebesgue_2Emeasure__absolutely__continuous,type,(c_2Elebesgue_2Emeasure__absolutely__continuous:del > $i)).
tff(mem_c_2Elebesgue_2Emeasure__absolutely__continuous,axiom,( ! [A_27a:del] : mem(c_2Elebesgue_2Emeasure__absolutely__continuous(A_27a),arr(ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),arr(ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),bool))))).
tff(tp_c_2Elebesgue_2Enegative__set,type,(c_2Elebesgue_2Enegative__set:del > $i)).
tff(mem_c_2Elebesgue_2Enegative__set,axiom,( ! [A_27a:del] : mem(c_2Elebesgue_2Enegative__set(A_27a),arr(ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),arr(arr(A_27a,bool),bool))))).
tff(tp_c_2Elebesgue_2Epos__fn__integral,type,(c_2Elebesgue_2Epos__fn__integral:del > $i)).
tff(mem_c_2Elebesgue_2Epos__fn__integral,axiom,( ! [A_27a:del] : mem(c_2Elebesgue_2Epos__fn__integral(A_27a),arr(ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),arr(arr(A_27a,ty_2Eextreal_2Eextreal),ty_2Eextreal_2Eextreal))))).
tff(tp_c_2Elebesgue_2Epos__simple__fn__integral,type,(c_2Elebesgue_2Epos__simple__fn__integral:del > $i)).
tff(mem_c_2Elebesgue_2Epos__simple__fn__integral,axiom,( ! [A_27a:del] : mem(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),arr(ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),arr(arr(ty_2Enum_2Enum,bool),arr(arr(ty_2Enum_2Enum,arr(A_27a,bool)),arr(arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal),ty_2Eextreal_2Eextreal))))))).
tff(tp_c_2Elebesgue_2Eprod__measure,type,(c_2Elebesgue_2Eprod__measure:(del * del) > $i)).
tff(mem_c_2Elebesgue_2Eprod__measure,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Elebesgue_2Eprod__measure(A_27a,A_27b),arr(ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),arr(ty_2Epair_2Eprod(arr(A_27b,bool),ty_2Epair_2Eprod(arr(arr(A_27b,bool),bool),arr(arr(A_27b,bool),ty_2Erealax_2Ereal))),arr(arr(ty_2Epair_2Eprod(A_27a,A_27b),bool),ty_2Erealax_2Ereal))))))).
tff(tp_c_2Elebesgue_2Eprod__measure3,type,(c_2Elebesgue_2Eprod__measure3:(del * del * del) > $i)).
tff(mem_c_2Elebesgue_2Eprod__measure3,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : ( ! [A_27c:del] : mem(c_2Elebesgue_2Eprod__measure3(A_27a,A_27b,A_27c),arr(ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),arr(ty_2Epair_2Eprod(arr(A_27b,bool),ty_2Epair_2Eprod(arr(arr(A_27b,bool),bool),arr(arr(A_27b,bool),ty_2Erealax_2Ereal))),arr(ty_2Epair_2Eprod(arr(A_27c,bool),ty_2Epair_2Eprod(arr(arr(A_27c,bool),bool),arr(arr(A_27c,bool),ty_2Erealax_2Ereal))),arr(arr(ty_2Epair_2Eprod(A_27a,ty_2Epair_2Eprod(A_27b,A_27c)),bool),ty_2Erealax_2Ereal))))))))).
tff(tp_c_2Elebesgue_2Eprod__measure__space,type,(c_2Elebesgue_2Eprod__measure__space:(del * del) > $i)).
tff(mem_c_2Elebesgue_2Eprod__measure__space,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Elebesgue_2Eprod__measure__space(A_27a,A_27b),arr(ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),arr(ty_2Epair_2Eprod(arr(A_27b,bool),ty_2Epair_2Eprod(arr(arr(A_27b,bool),bool),arr(arr(A_27b,bool),ty_2Erealax_2Ereal))),ty_2Epair_2Eprod(arr(ty_2Epair_2Eprod(A_27a,A_27b),bool),ty_2Epair_2Eprod(arr(arr(ty_2Epair_2Eprod(A_27a,A_27b),bool),bool),arr(arr(ty_2Epair_2Eprod(A_27a,A_27b),bool),ty_2Erealax_2Ereal))))))))).
tff(tp_c_2Elebesgue_2Eprod__measure__space3,type,(c_2Elebesgue_2Eprod__measure__space3:(del * del * del) > $i)).
tff(mem_c_2Elebesgue_2Eprod__measure__space3,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : ( ! [A_27c:del] : mem(c_2Elebesgue_2Eprod__measure__space3(A_27a,A_27b,A_27c),arr(ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),arr(ty_2Epair_2Eprod(arr(A_27b,bool),ty_2Epair_2Eprod(arr(arr(A_27b,bool),bool),arr(arr(A_27b,bool),ty_2Erealax_2Ereal))),arr(ty_2Epair_2Eprod(arr(A_27c,bool),ty_2Epair_2Eprod(arr(arr(A_27c,bool),bool),arr(arr(A_27c,bool),ty_2Erealax_2Ereal))),ty_2Epair_2Eprod(arr(ty_2Epair_2Eprod(A_27a,ty_2Epair_2Eprod(A_27b,A_27c)),bool),ty_2Epair_2Eprod(arr(arr(ty_2Epair_2Eprod(A_27a,ty_2Epair_2Eprod(A_27b,A_27c)),bool),bool),arr(arr(ty_2Epair_2Eprod(A_27a,ty_2Epair_2Eprod(A_27b,A_27c)),bool),ty_2Erealax_2Ereal))))))))))).
tff(tp_c_2Elebesgue_2Eprod__sets3,type,(c_2Elebesgue_2Eprod__sets3:(del * del * del) > $i)).
tff(mem_c_2Elebesgue_2Eprod__sets3,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : ( ! [A_27c:del] : mem(c_2Elebesgue_2Eprod__sets3(A_27a,A_27b,A_27c),arr(arr(arr(A_27a,bool),bool),arr(arr(arr(A_27b,bool),bool),arr(arr(arr(A_27c,bool),bool),arr(arr(ty_2Epair_2Eprod(A_27a,ty_2Epair_2Eprod(A_27b,A_27c)),bool),bool))))))))).
tff(tp_c_2Elebesgue_2Epsfis,type,(c_2Elebesgue_2Epsfis:del > $i)).
tff(mem_c_2Elebesgue_2Epsfis,axiom,( ! [A_27a:del] : mem(c_2Elebesgue_2Epsfis(A_27a),arr(ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),arr(arr(A_27a,ty_2Eextreal_2Eextreal),arr(ty_2Eextreal_2Eextreal,bool)))))).
tff(tp_c_2Elebesgue_2Epsfs,type,(c_2Elebesgue_2Epsfs:del > $i)).
tff(mem_c_2Elebesgue_2Epsfs,axiom,( ! [A_27a:del] : mem(c_2Elebesgue_2Epsfs(A_27a),arr(ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),arr(arr(A_27a,ty_2Eextreal_2Eextreal),arr(ty_2Epair_2Eprod(arr(ty_2Enum_2Enum,bool),ty_2Epair_2Eprod(arr(ty_2Enum_2Enum,arr(A_27a,bool)),arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal))),bool)))))).
tff(tp_c_2Elebesgue_2Eseq__sup,type,(c_2Elebesgue_2Eseq__sup:$i)).
tff(mem_c_2Elebesgue_2Eseq__sup,axiom,mem(c_2Elebesgue_2Eseq__sup,arr(arr(ty_2Eextreal_2Eextreal,bool),arr(ty_2Enum_2Enum,ty_2Eextreal_2Eextreal)))).
tff(tp_c_2Elebesgue_2Esigned__measure__space,type,(c_2Elebesgue_2Esigned__measure__space:del > $i)).
tff(mem_c_2Elebesgue_2Esigned__measure__space,axiom,( ! [A_27a:del] : mem(c_2Elebesgue_2Esigned__measure__space(A_27a),arr(ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),bool)))).
tff(ax_thm_2Elebesgue_2Epos__simple__fn__integral__def,axiom,( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1s:$i] : (mem(V1s,arr(ty_2Enum_2Enum,bool)) => ( ! [V2a:$i] : (mem(V2a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ( ! [V3x:$i] : (mem(V3x,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => (surj__ty_2Eextreal_2Eextreal(ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V1s),V2a),V3x)) = surj__ty_2Eextreal_2Eextreal(ap(c_2Eextreal_2ENormal,ap(ap(c_2Ereal__sigma_2EREAL__SUM__IMAGE(ty_2Enum_2Enum),f4078(A_27a,V0m,V2a,V3x)),V1s)))))))))))))).
tff(ax_thm_2Elebesgue_2Epsfs__def,axiom,( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => (ap(ap(c_2Elebesgue_2Epsfs(A_27a),V0m),V1f) = ap(c_2Epred__set_2EGSPEC(ty_2Epair_2Eprod(arr(ty_2Enum_2Enum,bool),ty_2Epair_2Eprod(arr(ty_2Enum_2Enum,arr(A_27a,bool)),arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal))),ty_2Epair_2Eprod(arr(ty_2Enum_2Enum,bool),ty_2Epair_2Eprod(arr(ty_2Enum_2Enum,arr(A_27a,bool)),arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)))),ap(c_2Epair_2EUNCURRY(arr(ty_2Enum_2Enum,bool),ty_2Epair_2Eprod(arr(ty_2Enum_2Enum,arr(A_27a,bool)),arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)),ty_2Epair_2Eprod(ty_2Epair_2Eprod(arr(ty_2Enum_2Enum,bool),ty_2Epair_2Eprod(arr(ty_2Enum_2Enum,arr(A_27a,bool)),arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal))),bool)),f4081(A_27a,V1f,V0m)))))))))).
tff(ax_thm_2Elebesgue_2Epsfis__def,axiom,( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => (ap(ap(c_2Elebesgue_2Epsfis(A_27a),V0m),V1f) = ap(ap(c_2Epred__set_2EIMAGE(ty_2Epair_2Eprod(arr(ty_2Enum_2Enum,bool),ty_2Epair_2Eprod(arr(ty_2Enum_2Enum,arr(A_27a,bool)),arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal))),ty_2Eextreal_2Eextreal),ap(c_2Epair_2EUNCURRY(arr(ty_2Enum_2Enum,bool),ty_2Epair_2Eprod(arr(ty_2Enum_2Enum,arr(A_27a,bool)),arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)),ty_2Eextreal_2Eextreal),f4084(A_27a,V0m))),ap(ap(c_2Elebesgue_2Epsfs(A_27a),V0m),V1f))))))))).
tff(ax_thm_2Elebesgue_2Epos__fn__integral__def,axiom,( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => (surj__ty_2Eextreal_2Eextreal(ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),V1f)) = surj__ty_2Eextreal_2Eextreal(ap(c_2Eextreal_2Eextreal__sup,ap(c_2Epred__set_2EGSPEC(ty_2Eextreal_2Eextreal,ty_2Eextreal_2Eextreal),f4087(A_27a,V0m,V1f))))))))))).
tff(ax_thm_2Elebesgue_2Eintegral__def,axiom,( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => (surj__ty_2Eextreal_2Eextreal(ap(ap(c_2Elebesgue_2Eintegral(A_27a),V0m),V1f)) = surj__ty_2Eextreal_2Eextreal(ap(ap(c_2Eextreal_2Eextreal__sub,ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),ap(c_2Emeasure_2Efn__plus(A_27a),V1f))),ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),ap(c_2Emeasure_2Efn__minus(A_27a),V1f))))))))))).
tff(ax_thm_2Elebesgue_2Eintegrable__def,axiom,( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => (p(ap(ap(c_2Elebesgue_2Eintegrable(A_27a),V0m),V1f)) <=> (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,ty_2Eextreal_2Eextreal)),V1f),ap(ap(c_2Emeasure_2Emeasurable(A_27a,ty_2Eextreal_2Eextreal),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),arr(arr(A_27a,bool),bool)),ap(c_2Emeasure_2Em__space(A_27a),V0m)),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m))),c_2Emeasure_2EBorel))) & ((~~ (surj__ty_2Eextreal_2Eextreal(ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),ap(c_2Emeasure_2Efn__plus(A_27a),V1f))) = fo__c_2Eextreal_2EPosInf)) & (~~ (surj__ty_2Eextreal_2Eextreal(ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),ap(c_2Emeasure_2Efn__minus(A_27a),V1f))) = fo__c_2Eextreal_2EPosInf))))))))))).
tff(ax_thm_2Elebesgue_2Efinite__space__integral__def,axiom,( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => (surj__ty_2Eextreal_2Eextreal(ap(ap(c_2Elebesgue_2Efinite__space__integral(A_27a),V0m),V1f)) = surj__ty_2Eextreal_2Eextreal(ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(ty_2Eextreal_2Eextreal),f4088(A_27a,V1f,V0m)),ap(ap(c_2Epred__set_2EIMAGE(A_27a,ty_2Eextreal_2Eextreal),V1f),ap(c_2Emeasure_2Em__space(A_27a),V0m))))))))))).
tff(ax_thm_2Elebesgue_2Eprod__measure__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0m0:$i] : (mem(V0m0,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1m1:$i] : (mem(V1m1,ty_2Epair_2Eprod(arr(A_27b,bool),ty_2Epair_2Eprod(arr(arr(A_27b,bool),bool),arr(arr(A_27b,bool),ty_2Erealax_2Ereal)))) => (ap(ap(c_2Elebesgue_2Eprod__measure(A_27a,A_27b),V0m0),V1m1) = f4091(A_27a,A_27b,V0m0,V1m1))))))))).
tff(ax_thm_2Elebesgue_2Eprod__measure__space__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0m0:$i] : (mem(V0m0,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1m1:$i] : (mem(V1m1,ty_2Epair_2Eprod(arr(A_27b,bool),ty_2Epair_2Eprod(arr(arr(A_27b,bool),bool),arr(arr(A_27b,bool),ty_2Erealax_2Ereal)))) => (ap(ap(c_2Elebesgue_2Eprod__measure__space(A_27a,A_27b),V0m0),V1m1) = ap(ap(c_2Epair_2E_2C(arr(ty_2Epair_2Eprod(A_27a,A_27b),bool),ty_2Epair_2Eprod(arr(arr(ty_2Epair_2Eprod(A_27a,A_27b),bool),bool),arr(arr(ty_2Epair_2Eprod(A_27a,A_27b),bool),ty_2Erealax_2Ereal))),ap(ap(c_2Epred__set_2ECROSS(A_27a,A_27b),ap(c_2Emeasure_2Em__space(A_27a),V0m0)),ap(c_2Emeasure_2Em__space(A_27b),V1m1))),ap(ap(c_2Epair_2E_2C(arr(arr(ty_2Epair_2Eprod(A_27a,A_27b),bool),bool),arr(arr(ty_2Epair_2Eprod(A_27a,A_27b),bool),ty_2Erealax_2Ereal)),ap(c_2Emeasure_2Esubsets(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Emeasure_2Esigma(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epred__set_2ECROSS(A_27a,A_27b),ap(c_2Emeasure_2Em__space(A_27a),V0m0)),ap(c_2Emeasure_2Em__space(A_27b),V1m1))),ap(ap(c_2Eutil__prob_2Eprod__sets(A_27a,A_27b),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m0)),ap(c_2Emeasure_2Emeasurable__sets(A_27b),V1m1))))),ap(ap(c_2Elebesgue_2Eprod__measure(A_27a,A_27b),V0m0),V1m1))))))))))).
tff(ax_thm_2Elebesgue_2Eprod__sets3__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0a:$i] : (mem(V0a,arr(arr(A_27a,bool),bool)) => ( ! [V1b:$i] : (mem(V1b,arr(arr(A_27b,bool),bool)) => ( ! [V2c:$i] : (mem(V2c,arr(arr(A_27c,bool),bool)) => (ap(ap(ap(c_2Elebesgue_2Eprod__sets3(A_27a,A_27b,A_27c),V0a),V1b),V2c) = ap(c_2Epred__set_2EGSPEC(arr(ty_2Epair_2Eprod(A_27a,ty_2Epair_2Eprod(A_27b,A_27c)),bool),ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(A_27b,bool),arr(A_27c,bool)))),ap(c_2Epair_2EUNCURRY(arr(A_27a,bool),ty_2Epair_2Eprod(arr(A_27b,bool),arr(A_27c,bool)),ty_2Epair_2Eprod(arr(ty_2Epair_2Eprod(A_27a,ty_2Epair_2Eprod(A_27b,A_27c)),bool),bool)),f4094(A_27c,A_27b,A_27a,V2c,V1b,V0a)))))))))))))).
tff(ax_thm_2Elebesgue_2Eprod__measure3__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0m0:$i] : (mem(V0m0,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1m1:$i] : (mem(V1m1,ty_2Epair_2Eprod(arr(A_27b,bool),ty_2Epair_2Eprod(arr(arr(A_27b,bool),bool),arr(arr(A_27b,bool),ty_2Erealax_2Ereal)))) => ( ! [V2m2:$i] : (mem(V2m2,ty_2Epair_2Eprod(arr(A_27c,bool),ty_2Epair_2Eprod(arr(arr(A_27c,bool),bool),arr(arr(A_27c,bool),ty_2Erealax_2Ereal)))) => (ap(ap(ap(c_2Elebesgue_2Eprod__measure3(A_27a,A_27b,A_27c),V0m0),V1m1),V2m2) = ap(ap(c_2Elebesgue_2Eprod__measure(A_27a,ty_2Epair_2Eprod(A_27b,A_27c)),V0m0),ap(ap(c_2Elebesgue_2Eprod__measure__space(A_27b,A_27c),V1m1),V2m2))))))))))))).
tff(ax_thm_2Elebesgue_2Eprod__measure__space3__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0m0:$i] : (mem(V0m0,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1m1:$i] : (mem(V1m1,ty_2Epair_2Eprod(arr(A_27b,bool),ty_2Epair_2Eprod(arr(arr(A_27b,bool),bool),arr(arr(A_27b,bool),ty_2Erealax_2Ereal)))) => ( ! [V2m2:$i] : (mem(V2m2,ty_2Epair_2Eprod(arr(A_27c,bool),ty_2Epair_2Eprod(arr(arr(A_27c,bool),bool),arr(arr(A_27c,bool),ty_2Erealax_2Ereal)))) => (ap(ap(ap(c_2Elebesgue_2Eprod__measure__space3(A_27a,A_27b,A_27c),V0m0),V1m1),V2m2) = ap(ap(c_2Epair_2E_2C(arr(ty_2Epair_2Eprod(A_27a,ty_2Epair_2Eprod(A_27b,A_27c)),bool),ty_2Epair_2Eprod(arr(arr(ty_2Epair_2Eprod(A_27a,ty_2Epair_2Eprod(A_27b,A_27c)),bool),bool),arr(arr(ty_2Epair_2Eprod(A_27a,ty_2Epair_2Eprod(A_27b,A_27c)),bool),ty_2Erealax_2Ereal))),ap(ap(c_2Epred__set_2ECROSS(A_27a,ty_2Epair_2Eprod(A_27b,A_27c)),ap(c_2Emeasure_2Em__space(A_27a),V0m0)),ap(ap(c_2Epred__set_2ECROSS(A_27b,A_27c),ap(c_2Emeasure_2Em__space(A_27b),V1m1)),ap(c_2Emeasure_2Em__space(A_27c),V2m2)))),ap(ap(c_2Epair_2E_2C(arr(arr(ty_2Epair_2Eprod(A_27a,ty_2Epair_2Eprod(A_27b,A_27c)),bool),bool),arr(arr(ty_2Epair_2Eprod(A_27a,ty_2Epair_2Eprod(A_27b,A_27c)),bool),ty_2Erealax_2Ereal)),ap(c_2Emeasure_2Esubsets(ty_2Epair_2Eprod(A_27a,ty_2Epair_2Eprod(A_27b,A_27c))),ap(ap(c_2Emeasure_2Esigma(ty_2Epair_2Eprod(A_27a,ty_2Epair_2Eprod(A_27b,A_27c))),ap(ap(c_2Epred__set_2ECROSS(A_27a,ty_2Epair_2Eprod(A_27b,A_27c)),ap(c_2Emeasure_2Em__space(A_27a),V0m0)),ap(ap(c_2Epred__set_2ECROSS(A_27b,A_27c),ap(c_2Emeasure_2Em__space(A_27b),V1m1)),ap(c_2Emeasure_2Em__space(A_27c),V2m2)))),ap(ap(ap(c_2Elebesgue_2Eprod__sets3(A_27a,A_27b,A_27c),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m0)),ap(c_2Emeasure_2Emeasurable__sets(A_27b),V1m1)),ap(c_2Emeasure_2Emeasurable__sets(A_27c),V2m2))))),ap(ap(ap(c_2Elebesgue_2Eprod__measure3(A_27a,A_27b,A_27c),V0m0),V1m1),V2m2)))))))))))))).
tff(conj_thm_2Elebesgue_2Epos__simple__fn__integral__present,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ! [V2s:$i] : (mem(V2s,arr(ty_2Enum_2Enum,bool)) => ( ! [V3a:$i] : (mem(V3a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ( ! [V4x:$i] : (mem(V4x,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ( ! [V5g:$i] : (mem(V5g,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ! [V6s_27:$i] : (mem(V6s_27,arr(ty_2Enum_2Enum,bool)) => ( ! [V7b:$i] : (mem(V7b,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ( ! [V8y:$i] : (mem(V8y,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ((p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & (p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V0m),V1f),V2s),V3a),V4x)) & p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V0m),V5g),V6s_27),V7b),V8y)))) => (? [V9z:$i] : (mem(V9z,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) & (? [V10z_27:$i] : (mem(V10z_27,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) & (? [V11c:$i] : (mem(V11c,arr(ty_2Enum_2Enum,arr(A_27a,bool))) & (? [V12k:$i] : (mem(V12k,arr(ty_2Enum_2Enum,bool)) & (( ! [V13t:$i] : (mem(V13t,A_27a) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V13t),ap(c_2Emeasure_2Em__space(A_27a),V0m))) => (surj__ty_2Eextreal_2Eextreal(ap(V1f,V13t)) = surj__ty_2Eextreal_2Eextreal(ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(ty_2Enum_2Enum),f4095(A_27a,V13t,V11c,V9z)),V12k)))))) & (( ! [V15t:$i] : (mem(V15t,A_27a) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V15t),ap(c_2Emeasure_2Em__space(A_27a),V0m))) => (surj__ty_2Eextreal_2Eextreal(ap(V5g,V15t)) = surj__ty_2Eextreal_2Eextreal(ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(ty_2Enum_2Enum),f4096(A_27a,V15t,V11c,V10z_27)),V12k)))))) & ((surj__ty_2Eextreal_2Eextreal(ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V2s),V3a),V4x)) = surj__ty_2Eextreal_2Eextreal(ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V12k),V11c),V9z))) & ((surj__ty_2Eextreal_2Eextreal(ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V6s_27),V7b),V8y)) = surj__ty_2Eextreal_2Eextreal(ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V12k),V11c),V10z_27))) & (p(ap(c_2Epred__set_2EFINITE(ty_2Enum_2Enum),V12k)) & (( ! [V17i:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V17i)),V12k)) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(V9z,inj__ty_2Enum_2Enum(V17i)))))) & (( ! [V18i:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V18i)),V12k)) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(V10z_27,inj__ty_2Enum_2Enum(V18i)))))) & (( ! [V19i:tp__ty_2Enum_2Enum] : ( ! [V20j:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V19i)),V12k)) & (p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V20j)),V12k)) & (~~ (V19i = V20j)))) => p(ap(ap(c_2Epred__set_2EDISJOINT(A_27a),ap(V11c,inj__ty_2Enum_2Enum(V19i))),ap(V11c,inj__ty_2Enum_2Enum(V20j))))))) & (( ! [V21i:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V21i)),V12k)) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(V11c,inj__ty_2Enum_2Enum(V21i))),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m))))) & (ap(c_2Epred__set_2EBIGUNION(A_27a),ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,arr(A_27a,bool)),V11c),V12k)) = ap(c_2Emeasure_2Em__space(A_27a),V0m))))))))))))))))))))))))))))))))))))))))).
tff(conj_thm_2Elebesgue_2Epsfis__present,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ! [V2g:$i] : (mem(V2g,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ! [V3a:tp__ty_2Eextreal_2Eextreal] : ( ! [V4b:tp__ty_2Eextreal_2Eextreal] : ((p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & (p(ap(ap(c_2Ebool_2EIN(ty_2Eextreal_2Eextreal),inj__ty_2Eextreal_2Eextreal(V3a)),ap(ap(c_2Elebesgue_2Epsfis(A_27a),V0m),V1f))) & p(ap(ap(c_2Ebool_2EIN(ty_2Eextreal_2Eextreal),inj__ty_2Eextreal_2Eextreal(V4b)),ap(ap(c_2Elebesgue_2Epsfis(A_27a),V0m),V2g))))) => (? [V5z:$i] : (mem(V5z,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) & (? [V6z_27:$i] : (mem(V6z_27,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) & (? [V7c:$i] : (mem(V7c,arr(ty_2Enum_2Enum,arr(A_27a,bool))) & (? [V8k:$i] : (mem(V8k,arr(ty_2Enum_2Enum,bool)) & (( ! [V9t:$i] : (mem(V9t,A_27a) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V9t),ap(c_2Emeasure_2Em__space(A_27a),V0m))) => (surj__ty_2Eextreal_2Eextreal(ap(V1f,V9t)) = surj__ty_2Eextreal_2Eextreal(ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(ty_2Enum_2Enum),f4097(A_27a,V9t,V7c,V5z)),V8k)))))) & (( ! [V11t:$i] : (mem(V11t,A_27a) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V11t),ap(c_2Emeasure_2Em__space(A_27a),V0m))) => (surj__ty_2Eextreal_2Eextreal(ap(V2g,V11t)) = surj__ty_2Eextreal_2Eextreal(ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(ty_2Enum_2Enum),f4098(A_27a,V11t,V7c,V6z_27)),V8k)))))) & ((V3a = surj__ty_2Eextreal_2Eextreal(ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V8k),V7c),V5z))) & ((V4b = surj__ty_2Eextreal_2Eextreal(ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V8k),V7c),V6z_27))) & (p(ap(c_2Epred__set_2EFINITE(ty_2Enum_2Enum),V8k)) & (( ! [V13i:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V13i)),V8k)) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(V5z,inj__ty_2Enum_2Enum(V13i)))))) & (( ! [V14i:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V14i)),V8k)) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(V6z_27,inj__ty_2Enum_2Enum(V14i)))))) & (( ! [V15i:tp__ty_2Enum_2Enum] : ( ! [V16j:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V15i)),V8k)) & (p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V16j)),V8k)) & (~~ (V15i = V16j)))) => p(ap(ap(c_2Epred__set_2EDISJOINT(A_27a),ap(V7c,inj__ty_2Enum_2Enum(V15i))),ap(V7c,inj__ty_2Enum_2Enum(V16j))))))) & (( ! [V17i:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V17i)),V8k)) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(V7c,inj__ty_2Enum_2Enum(V17i))),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m))))) & (ap(c_2Epred__set_2EBIGUNION(A_27a),ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,arr(A_27a,bool)),V7c),V8k)) = ap(c_2Emeasure_2Em__space(A_27a),V0m))))))))))))))))))))))))))))))).
tff(conj_thm_2Elebesgue_2Epos__simple__fn__thm1,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ! [V2s:$i] : (mem(V2s,arr(ty_2Enum_2Enum,bool)) => ( ! [V3a:$i] : (mem(V3a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ( ! [V4x:$i] : (mem(V4x,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ( ! [V5i:tp__ty_2Enum_2Enum] : ( ! [V6y:$i] : (mem(V6y,A_27a) => ((p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & (p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V0m),V1f),V2s),V3a),V4x)) & (p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V5i)),V2s)) & p(ap(ap(c_2Ebool_2EIN(A_27a),V6y),ap(V3a,inj__ty_2Enum_2Enum(V5i))))))) => (surj__ty_2Eextreal_2Eextreal(ap(V1f,V6y)) = surj__ty_2Eextreal_2Eextreal(ap(c_2Eextreal_2ENormal,ap(V4x,inj__ty_2Enum_2Enum(V5i)))))))))))))))))))))).
tff(conj_thm_2Elebesgue_2Epos__simple__fn__le,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ! [V2g:$i] : (mem(V2g,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ! [V3s:$i] : (mem(V3s,arr(ty_2Enum_2Enum,bool)) => ( ! [V4a:$i] : (mem(V4a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ( ! [V5x:$i] : (mem(V5x,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ( ! [V6x_27:$i] : (mem(V6x_27,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ( ! [V7i:tp__ty_2Enum_2Enum] : ((p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & (p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V0m),V1f),V3s),V4a),V5x)) & (p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V0m),V2g),V3s),V4a),V6x_27)) & (( ! [V8x:$i] : (mem(V8x,A_27a) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V8x),ap(c_2Emeasure_2Em__space(A_27a),V0m))) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(V2g,V8x)),ap(V1f,V8x)))))) & (p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V7i)),V3s)) & (~~ (ap(V4a,inj__ty_2Enum_2Enum(V7i)) = c_2Epred__set_2EEMPTY(A_27a)))))))) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2ENormal,ap(V6x_27,inj__ty_2Enum_2Enum(V7i)))),ap(c_2Eextreal_2ENormal,ap(V5x,inj__ty_2Enum_2Enum(V7i)))))))))))))))))))))))).
tff(conj_thm_2Elebesgue_2Epos__simple__fn__cmul,lemma,(( ! [A_27a:del]: ( ! [V0s:$i] : (mem(V0s,arr(ty_2Enum_2Enum,bool)) => ( ! [V1a:$i] : (mem(V1a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ( ! [V2x:$i] : (mem(V2x,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ( ! [V3m:$i] : (mem(V3m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V4f:$i] : (mem(V4f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ! [V5z:tp__ty_2Erealax_2Ereal] : ((p(ap(c_2Emeasure_2Emeasure__space(A_27a),V3m)) & (p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V3m),V4f),V0s),V1a),V2x)) & p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Erealax_2Ereal(V5z))))) => (? [V6s_27:$i] : (mem(V6s_27,arr(ty_2Enum_2Enum,bool)) & (? [V7a_27:$i] : (mem(V7a_27,arr(ty_2Enum_2Enum,arr(A_27a,bool))) & (? [V8x_27:$i] : (mem(V8x_27,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) & p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V3m),f4099(A_27a,V4f,V5z)),V6s_27),V7a_27),V8x_27))))))))))))))))))))))).
tff(conj_thm_2Elebesgue_2Epos__simple__fn__cmul__alt,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ! [V2s:$i] : (mem(V2s,arr(ty_2Enum_2Enum,bool)) => ( ! [V3a:$i] : (mem(V3a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ( ! [V4x:$i] : (mem(V4x,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ( ! [V5z:tp__ty_2Erealax_2Ereal] : ((p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & (p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Erealax_2Ereal(V5z))) & p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V0m),V1f),V2s),V3a),V4x)))) => p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V0m),f4100(A_27a,V1f,V5z)),V2s),V3a),f4101(V4x,V5z)))))))))))))))))).
tff(conj_thm_2Elebesgue_2Epos__simple__fn__add,lemma,(( ! [A_27a:del]: ( ! [V0s:$i] : (mem(V0s,arr(ty_2Enum_2Enum,bool)) => ( ! [V1a:$i] : (mem(V1a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ( ! [V2x:$i] : (mem(V2x,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ( ! [V3s_27:$i] : (mem(V3s_27,arr(ty_2Enum_2Enum,bool)) => ( ! [V4a_27:$i] : (mem(V4a_27,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ( ! [V5x_27:$i] : (mem(V5x_27,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ( ! [V6m:$i] : (mem(V6m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V7f:$i] : (mem(V7f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ! [V8g:$i] : (mem(V8g,arr(A_27a,ty_2Eextreal_2Eextreal)) => ((p(ap(c_2Emeasure_2Emeasure__space(A_27a),V6m)) & (p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V6m),V7f),V0s),V1a),V2x)) & p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V6m),V8g),V3s_27),V4a_27),V5x_27)))) => (? [V9s_27_27:$i] : (mem(V9s_27_27,arr(ty_2Enum_2Enum,bool)) & (? [V10a_27_27:$i] : (mem(V10a_27_27,arr(ty_2Enum_2Enum,arr(A_27a,bool))) & (? [V11x_27_27:$i] : (mem(V11x_27_27,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) & p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V6m),f4102(A_27a,V7f,V8g)),V9s_27_27),V10a_27_27),V11x_27_27)))))))))))))))))))))))))))))).
tff(conj_thm_2Elebesgue_2Epos__simple__fn__add__alt,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ! [V2g:$i] : (mem(V2g,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ! [V3s:$i] : (mem(V3s,arr(ty_2Enum_2Enum,bool)) => ( ! [V4a:$i] : (mem(V4a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ( ! [V5x:$i] : (mem(V5x,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ( ! [V6y:$i] : (mem(V6y,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ((p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & (p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V0m),V1f),V3s),V4a),V5x)) & p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V0m),V2g),V3s),V4a),V6y)))) => p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V0m),f4103(A_27a,V1f,V2g)),V3s),V4a),f4104(V5x,V6y))))))))))))))))))))).
tff(conj_thm_2Elebesgue_2Epos__simple__fn__indicator,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1A:$i] : (mem(V1A,arr(A_27a,bool)) => ((p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V1A),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m)))) => (? [V2s:$i] : (mem(V2s,arr(ty_2Enum_2Enum,bool)) & (? [V3a:$i] : (mem(V3a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) & (? [V4x:$i] : (mem(V4x,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) & p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V0m),ap(c_2Emeasure_2Eindicator__fn(A_27a),V1A)),V2s),V3a),V4x)))))))))))))))).
tff(conj_thm_2Elebesgue_2Epos__simple__fn__indicator__alt,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => ((p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V1s),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m)))) => p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V0m),ap(c_2Emeasure_2Eindicator__fn(A_27a),V1s)),ap(ap(c_2Epred__set_2EINSERT(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(ap(c_2Epred__set_2EINSERT(ty_2Enum_2Enum),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),c_2Epred__set_2EEMPTY(ty_2Enum_2Enum)))),f4105(A_27a,V0m,V1s)),f4106)))))))))).
tff(conj_thm_2Elebesgue_2Epos__simple__fn__max,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s_27:$i] : (mem(V0s_27,arr(ty_2Enum_2Enum,bool)) => ( ! [V1b:$i] : (mem(V1b,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ( ! [V2m:$i] : (mem(V2m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V3f:$i] : (mem(V3f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ! [V4s:$i] : (mem(V4s,arr(ty_2Enum_2Enum,bool)) => ( ! [V5a:$i] : (mem(V5a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ( ! [V6x:$i] : (mem(V6x,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ( ! [V7g:$i] : (mem(V7g,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ! [V8s_27b:$i] : (mem(V8s_27b,A_27b) => ( ! [V9y:$i] : (mem(V9y,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ((p(ap(c_2Emeasure_2Emeasure__space(A_27a),V2m)) & (p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V2m),V3f),V4s),V5a),V6x)) & p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V2m),V7g),V0s_27),V1b),V9y)))) => (? [V10s_27_27:$i] : (mem(V10s_27_27,arr(ty_2Enum_2Enum,bool)) & (? [V11a_27_27:$i] : (mem(V11a_27_27,arr(ty_2Enum_2Enum,arr(A_27a,bool))) & (? [V12x_27_27:$i] : (mem(V12x_27_27,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) & p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V2m),f4107(A_27a,V3f,V7g)),V10s_27_27),V11a_27_27),V12x_27_27))))))))))))))))))))))))))))))))).
tff(conj_thm_2Elebesgue_2Epos__simple__fn__not__infty,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ! [V2s:$i] : (mem(V2s,arr(ty_2Enum_2Enum,bool)) => ( ! [V3a:$i] : (mem(V3a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ( ! [V4x:$i] : (mem(V4x,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => (p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V0m),V1f),V2s),V3a),V4x)) => ( ! [V5x:$i] : (mem(V5x,A_27a) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V5x),ap(c_2Emeasure_2Em__space(A_27a),V0m))) => ((~~ (surj__ty_2Eextreal_2Eextreal(ap(V1f,V5x)) = fo__c_2Eextreal_2ENegInf)) & (~~ (surj__ty_2Eextreal_2Eextreal(ap(V1f,V5x)) = fo__c_2Eextreal_2EPosInf)))))))))))))))))))).
tff(conj_thm_2Elebesgue_2Epos__simple__fn__integral__add,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ! [V2s:$i] : (mem(V2s,arr(ty_2Enum_2Enum,bool)) => ( ! [V3a:$i] : (mem(V3a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ( ! [V4x:$i] : (mem(V4x,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ( ! [V5g:$i] : (mem(V5g,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ! [V6s_27:$i] : (mem(V6s_27,arr(ty_2Enum_2Enum,bool)) => ( ! [V7b:$i] : (mem(V7b,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ( ! [V8y:$i] : (mem(V8y,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ((p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & (p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V0m),V1f),V2s),V3a),V4x)) & p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V0m),V5g),V6s_27),V7b),V8y)))) => (? [V9s_27_27:$i] : (mem(V9s_27_27,arr(ty_2Enum_2Enum,bool)) & (? [V10c:$i] : (mem(V10c,arr(ty_2Enum_2Enum,arr(A_27a,bool))) & (? [V11z:$i] : (mem(V11z,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) & (p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V0m),f4108(A_27a,V1f,V5g)),V9s_27_27),V10c),V11z)) & (surj__ty_2Eextreal_2Eextreal(ap(ap(c_2Eextreal_2Eextreal__add,ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V2s),V3a),V4x)),ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V6s_27),V7b),V8y))) = surj__ty_2Eextreal_2Eextreal(ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V9s_27_27),V10c),V11z)))))))))))))))))))))))))))))))).
tff(conj_thm_2Elebesgue_2Epos__simple__fn__integral__add__alt,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ! [V2s:$i] : (mem(V2s,arr(ty_2Enum_2Enum,bool)) => ( ! [V3a:$i] : (mem(V3a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ( ! [V4x:$i] : (mem(V4x,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ( ! [V5g:$i] : (mem(V5g,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ! [V6y:$i] : (mem(V6y,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ((p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & (p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V0m),V1f),V2s),V3a),V4x)) & p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V0m),V5g),V2s),V3a),V6y)))) => (surj__ty_2Eextreal_2Eextreal(ap(ap(c_2Eextreal_2Eextreal__add,ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V2s),V3a),V4x)),ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V2s),V3a),V6y))) = surj__ty_2Eextreal_2Eextreal(ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V2s),V3a),f4109(V4x,V6y)))))))))))))))))))))).
tff(conj_thm_2Elebesgue_2Epsfis__add,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ! [V2g:$i] : (mem(V2g,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ! [V3a:tp__ty_2Eextreal_2Eextreal] : ( ! [V4b:tp__ty_2Eextreal_2Eextreal] : ((p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & (p(ap(ap(c_2Ebool_2EIN(ty_2Eextreal_2Eextreal),inj__ty_2Eextreal_2Eextreal(V3a)),ap(ap(c_2Elebesgue_2Epsfis(A_27a),V0m),V1f))) & p(ap(ap(c_2Ebool_2EIN(ty_2Eextreal_2Eextreal),inj__ty_2Eextreal_2Eextreal(V4b)),ap(ap(c_2Elebesgue_2Epsfis(A_27a),V0m),V2g))))) => p(ap(ap(c_2Ebool_2EIN(ty_2Eextreal_2Eextreal),ap(ap(c_2Eextreal_2Eextreal__add,inj__ty_2Eextreal_2Eextreal(V3a)),inj__ty_2Eextreal_2Eextreal(V4b))),ap(ap(c_2Elebesgue_2Epsfis(A_27a),V0m),f4110(A_27a,V1f,V2g)))))))))))))))).
tff(conj_thm_2Elebesgue_2Epos__simple__fn__integral__mono,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ! [V2s:$i] : (mem(V2s,arr(ty_2Enum_2Enum,bool)) => ( ! [V3a:$i] : (mem(V3a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ( ! [V4x:$i] : (mem(V4x,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ( ! [V5g:$i] : (mem(V5g,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ! [V6s_27:$i] : (mem(V6s_27,arr(ty_2Enum_2Enum,bool)) => ( ! [V7b:$i] : (mem(V7b,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ( ! [V8y:$i] : (mem(V8y,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ((p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & (p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V0m),V1f),V2s),V3a),V4x)) & (p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V0m),V5g),V6s_27),V7b),V8y)) & ( ! [V9x:$i] : (mem(V9x,A_27a) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V9x),ap(c_2Emeasure_2Em__space(A_27a),V0m))) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(V1f,V9x)),ap(V5g,V9x))))))))) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V2s),V3a),V4x)),ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V6s_27),V7b),V8y))))))))))))))))))))))))).
tff(conj_thm_2Elebesgue_2Epsfis__mono,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ! [V2g:$i] : (mem(V2g,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ! [V3a:tp__ty_2Eextreal_2Eextreal] : ( ! [V4b:tp__ty_2Eextreal_2Eextreal] : ((p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & (p(ap(ap(c_2Ebool_2EIN(ty_2Eextreal_2Eextreal),inj__ty_2Eextreal_2Eextreal(V3a)),ap(ap(c_2Elebesgue_2Epsfis(A_27a),V0m),V1f))) & (p(ap(ap(c_2Ebool_2EIN(ty_2Eextreal_2Eextreal),inj__ty_2Eextreal_2Eextreal(V4b)),ap(ap(c_2Elebesgue_2Epsfis(A_27a),V0m),V2g))) & ( ! [V5x:$i] : (mem(V5x,A_27a) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V5x),ap(c_2Emeasure_2Em__space(A_27a),V0m))) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(V1f,V5x)),ap(V2g,V5x))))))))) => p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(V3a)),inj__ty_2Eextreal_2Eextreal(V4b))))))))))))))).
tff(conj_thm_2Elebesgue_2Epos__simple__fn__integral__unique,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ! [V2s:$i] : (mem(V2s,arr(ty_2Enum_2Enum,bool)) => ( ! [V3a:$i] : (mem(V3a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ( ! [V4x:$i] : (mem(V4x,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ( ! [V5s_27:$i] : (mem(V5s_27,arr(ty_2Enum_2Enum,bool)) => ( ! [V6b:$i] : (mem(V6b,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ( ! [V7y:$i] : (mem(V7y,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ((p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & (p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V0m),V1f),V2s),V3a),V4x)) & p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V0m),V1f),V5s_27),V6b),V7y)))) => (surj__ty_2Eextreal_2Eextreal(ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V2s),V3a),V4x)) = surj__ty_2Eextreal_2Eextreal(ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V5s_27),V6b),V7y))))))))))))))))))))))).
tff(conj_thm_2Elebesgue_2Epsfis__unique,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ! [V2a:tp__ty_2Eextreal_2Eextreal] : ( ! [V3b:tp__ty_2Eextreal_2Eextreal] : ((p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & (p(ap(ap(c_2Ebool_2EIN(ty_2Eextreal_2Eextreal),inj__ty_2Eextreal_2Eextreal(V2a)),ap(ap(c_2Elebesgue_2Epsfis(A_27a),V0m),V1f))) & p(ap(ap(c_2Ebool_2EIN(ty_2Eextreal_2Eextreal),inj__ty_2Eextreal_2Eextreal(V3b)),ap(ap(c_2Elebesgue_2Epsfis(A_27a),V0m),V1f))))) => (V2a = V3b))))))))))).
tff(conj_thm_2Elebesgue_2Epos__simple__fn__integral__indicator,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1A:$i] : (mem(V1A,arr(A_27a,bool)) => ((p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V1A),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m)))) => (? [V2s:$i] : (mem(V2s,arr(ty_2Enum_2Enum,bool)) & (? [V3a:$i] : (mem(V3a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) & (? [V4x:$i] : (mem(V4x,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) & (p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V0m),ap(c_2Emeasure_2Eindicator__fn(A_27a),V1A)),V2s),V3a),V4x)) & (surj__ty_2Eextreal_2Eextreal(ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V2s),V3a),V4x)) = surj__ty_2Eextreal_2Eextreal(ap(c_2Eextreal_2ENormal,ap(ap(c_2Emeasure_2Emeasure(A_27a),V0m),V1A))))))))))))))))))).
tff(conj_thm_2Elebesgue_2Epsfis__indicator,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1A:$i] : (mem(V1A,arr(A_27a,bool)) => ((p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V1A),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m)))) => p(ap(ap(c_2Ebool_2EIN(ty_2Eextreal_2Eextreal),ap(c_2Eextreal_2ENormal,ap(ap(c_2Emeasure_2Emeasure(A_27a),V0m),V1A))),ap(ap(c_2Elebesgue_2Epsfis(A_27a),V0m),ap(c_2Emeasure_2Eindicator__fn(A_27a),V1A)))))))))))).
tff(conj_thm_2Elebesgue_2Epos__simple__fn__integral__cmul,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ! [V2s:$i] : (mem(V2s,arr(ty_2Enum_2Enum,bool)) => ( ! [V3a:$i] : (mem(V3a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ( ! [V4x:$i] : (mem(V4x,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ( ! [V5z:tp__ty_2Erealax_2Ereal] : ((p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & (p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V0m),V1f),V2s),V3a),V4x)) & p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Erealax_2Ereal(V5z))))) => (p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V0m),f4111(A_27a,V1f,V5z)),V2s),V3a),f4101(V4x,V5z))) & (surj__ty_2Eextreal_2Eextreal(ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V2s),V3a),f4112(V4x,V5z))) = surj__ty_2Eextreal_2Eextreal(ap(ap(c_2Eextreal_2Eextreal__mul,ap(c_2Eextreal_2ENormal,inj__ty_2Erealax_2Ereal(V5z))),ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V2s),V3a),V4x)))))))))))))))))))).
tff(conj_thm_2Elebesgue_2Epsfis__cmul,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ! [V2a:tp__ty_2Eextreal_2Eextreal] : ( ! [V3z:tp__ty_2Erealax_2Ereal] : ((p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & (p(ap(ap(c_2Ebool_2EIN(ty_2Eextreal_2Eextreal),inj__ty_2Eextreal_2Eextreal(V2a)),ap(ap(c_2Elebesgue_2Epsfis(A_27a),V0m),V1f))) & p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Erealax_2Ereal(V3z))))) => p(ap(ap(c_2Ebool_2EIN(ty_2Eextreal_2Eextreal),ap(ap(c_2Eextreal_2Eextreal__mul,ap(c_2Eextreal_2ENormal,inj__ty_2Erealax_2Ereal(V3z))),inj__ty_2Eextreal_2Eextreal(V2a))),ap(ap(c_2Elebesgue_2Epsfis(A_27a),V0m),f4113(A_27a,V1f,V3z)))))))))))))).
tff(conj_thm_2Elebesgue_2Epos__simple__fn__integral__cmul__alt,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ! [V2s:$i] : (mem(V2s,arr(ty_2Enum_2Enum,bool)) => ( ! [V3a:$i] : (mem(V3a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ( ! [V4x:$i] : (mem(V4x,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ( ! [V5z:tp__ty_2Erealax_2Ereal] : ((p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & (p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Erealax_2Ereal(V5z))) & p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V0m),V1f),V2s),V3a),V4x)))) => (? [V6s_27:$i] : (mem(V6s_27,arr(ty_2Enum_2Enum,bool)) & (? [V7a_27:$i] : (mem(V7a_27,arr(ty_2Enum_2Enum,arr(A_27a,bool))) & (? [V8x_27:$i] : (mem(V8x_27,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) & (p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V0m),f4114(A_27a,V1f,V5z)),V6s_27),V7a_27),V8x_27)) & (surj__ty_2Eextreal_2Eextreal(ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V6s_27),V7a_27),V8x_27)) = surj__ty_2Eextreal_2Eextreal(ap(ap(c_2Eextreal_2Eextreal__mul,ap(c_2Eextreal_2ENormal,inj__ty_2Erealax_2Ereal(V5z))),ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V2s),V3a),V4x)))))))))))))))))))))))))).
tff(conj_thm_2Elebesgue_2EIN__psfis,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1r:tp__ty_2Eextreal_2Eextreal] : ( ! [V2f:$i] : (mem(V2f,arr(A_27a,ty_2Eextreal_2Eextreal)) => (p(ap(ap(c_2Ebool_2EIN(ty_2Eextreal_2Eextreal),inj__ty_2Eextreal_2Eextreal(V1r)),ap(ap(c_2Elebesgue_2Epsfis(A_27a),V0m),V2f))) => (? [V3s:$i] : (mem(V3s,arr(ty_2Enum_2Enum,bool)) & (? [V4a:$i] : (mem(V4a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) & (? [V5x:$i] : (mem(V5x,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) & (p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V0m),V2f),V3s),V4a),V5x)) & (V1r = surj__ty_2Eextreal_2Eextreal(ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V3s),V4a),V5x))))))))))))))))))).
tff(conj_thm_2Elebesgue_2EIN__psfis__eq,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1r:tp__ty_2Eextreal_2Eextreal] : ( ! [V2f:$i] : (mem(V2f,arr(A_27a,ty_2Eextreal_2Eextreal)) => (p(ap(ap(c_2Ebool_2EIN(ty_2Eextreal_2Eextreal),inj__ty_2Eextreal_2Eextreal(V1r)),ap(ap(c_2Elebesgue_2Epsfis(A_27a),V0m),V2f))) <=> (? [V3s:$i] : (mem(V3s,arr(ty_2Enum_2Enum,bool)) & (? [V4a:$i] : (mem(V4a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) & (? [V5x:$i] : (mem(V5x,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) & (p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V0m),V2f),V3s),V4a),V5x)) & (V1r = surj__ty_2Eextreal_2Eextreal(ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V3s),V4a),V5x))))))))))))))))))).
tff(conj_thm_2Elebesgue_2Epsfis__pos,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ! [V2a:tp__ty_2Eextreal_2Eextreal] : ((p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & p(ap(ap(c_2Ebool_2EIN(ty_2Eextreal_2Eextreal),inj__ty_2Eextreal_2Eextreal(V2a)),ap(ap(c_2Elebesgue_2Epsfis(A_27a),V0m),V1f)))) => ( ! [V3x:$i] : (mem(V3x,A_27a) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V3x),ap(c_2Emeasure_2Em__space(A_27a),V0m))) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(V1f,V3x))))))))))))))).
tff(conj_thm_2Elebesgue_2Epos__simple__fn__integral__zero,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1s:$i] : (mem(V1s,arr(ty_2Enum_2Enum,bool)) => ( ! [V2a:$i] : (mem(V2a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ( ! [V3x:$i] : (mem(V3x,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ((p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V0m),k(A_27a,ap(c_2Eextreal_2Eextreal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))),V1s),V2a),V3x))) => (surj__ty_2Eextreal_2Eextreal(ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V1s),V2a),V3x)) = surj__ty_2Eextreal_2Eextreal(ap(c_2Eextreal_2Eextreal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))))))))))).
tff(conj_thm_2Elebesgue_2Epos__simple__fn__integral__zero__alt,lemma,(( ! [A_27a:del]: ( ! [V0g:$i] : (mem(V0g,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ! [V1m:$i] : (mem(V1m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V2s:$i] : (mem(V2s,arr(ty_2Enum_2Enum,bool)) => ( ! [V3a:$i] : (mem(V3a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ( ! [V4x:$i] : (mem(V4x,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ((p(ap(c_2Emeasure_2Emeasure__space(A_27a),V1m)) & (p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V1m),V0g),V2s),V3a),V4x)) & ( ! [V5x:$i] : (mem(V5x,A_27a) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V5x),ap(c_2Emeasure_2Em__space(A_27a),V1m))) => (surj__ty_2Eextreal_2Eextreal(ap(V0g,V5x)) = surj__ty_2Eextreal_2Eextreal(ap(c_2Eextreal_2Eextreal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))))) => (surj__ty_2Eextreal_2Eextreal(ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V1m),V2s),V3a),V4x)) = surj__ty_2Eextreal_2Eextreal(ap(c_2Eextreal_2Eextreal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))))))))))))).
tff(conj_thm_2Elebesgue_2Epsfis__zero,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1a:tp__ty_2Eextreal_2Eextreal] : (p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) => (p(ap(ap(c_2Ebool_2EIN(ty_2Eextreal_2Eextreal),inj__ty_2Eextreal_2Eextreal(V1a)),ap(ap(c_2Elebesgue_2Epsfis(A_27a),V0m),k(A_27a,ap(c_2Eextreal_2Eextreal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))) <=> (V1a = surj__ty_2Eextreal_2Eextreal(ap(c_2Eextreal_2Eextreal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))))))).
tff(conj_thm_2Elebesgue_2Epos__simple__fn__integral__not__infty,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1s:$i] : (mem(V1s,arr(ty_2Enum_2Enum,bool)) => ( ! [V2a:$i] : (mem(V2a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ( ! [V3x:$i] : (mem(V3x,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ((~~ (surj__ty_2Eextreal_2Eextreal(ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V1s),V2a),V3x)) = fo__c_2Eextreal_2ENegInf)) & (~~ (surj__ty_2Eextreal_2Eextreal(ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V1s),V2a),V3x)) = fo__c_2Eextreal_2EPosInf)))))))))))))).
tff(conj_thm_2Elebesgue_2Epsfis__not__infty,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ! [V2a:tp__ty_2Eextreal_2Eextreal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Eextreal_2Eextreal),inj__ty_2Eextreal_2Eextreal(V2a)),ap(ap(c_2Elebesgue_2Epsfis(A_27a),V0m),V1f))) => ((~~ (V2a = fo__c_2Eextreal_2ENegInf)) & (~~ (V2a = fo__c_2Eextreal_2EPosInf)))))))))))).
tff(conj_thm_2Elebesgue_2Epos__simple__fn__integral__sum,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1f:$i] : (mem(V1f,arr(A_27b,arr(A_27a,ty_2Eextreal_2Eextreal))) => ( ! [V2s:$i] : (mem(V2s,arr(ty_2Enum_2Enum,bool)) => ( ! [V3a:$i] : (mem(V3a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ( ! [V4x:$i] : (mem(V4x,arr(A_27b,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal))) => ( ! [V5P:$i] : (mem(V5P,arr(A_27b,bool)) => ((p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & (( ! [V6i:$i] : (mem(V6i,A_27b) => (p(ap(ap(c_2Ebool_2EIN(A_27b),V6i),V5P)) => p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V0m),ap(V1f,V6i)),V2s),V3a),ap(V4x,V6i)))))) & (p(ap(c_2Epred__set_2EFINITE(A_27b),V5P)) & (~~ (V5P = c_2Epred__set_2EEMPTY(A_27b)))))) => (p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V0m),f4116(A_27a,A_27b,V1f,V5P)),V2s),V3a),f4118(A_27b,V4x,V5P))) & (surj__ty_2Eextreal_2Eextreal(ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V2s),V3a),f4120(A_27b,V4x,V5P))) = surj__ty_2Eextreal_2Eextreal(ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27b),f4121(A_27a,A_27b,V3a,V0m,V2s,V4x)),V5P))))))))))))))))))))).
tff(conj_thm_2Elebesgue_2Epos__simple__fn__integral__sum__alt,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1f:$i] : (mem(V1f,arr(A_27b,arr(A_27a,ty_2Eextreal_2Eextreal))) => ( ! [V2s:$i] : (mem(V2s,arr(A_27b,arr(ty_2Enum_2Enum,bool))) => ( ! [V3a:$i] : (mem(V3a,arr(A_27b,arr(ty_2Enum_2Enum,arr(A_27a,bool)))) => ( ! [V4x:$i] : (mem(V4x,arr(A_27b,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal))) => ( ! [V5P:$i] : (mem(V5P,arr(A_27b,bool)) => ((p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & (( ! [V6i:$i] : (mem(V6i,A_27b) => (p(ap(ap(c_2Ebool_2EIN(A_27b),V6i),V5P)) => p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V0m),ap(V1f,V6i)),ap(V2s,V6i)),ap(V3a,V6i)),ap(V4x,V6i)))))) & (p(ap(c_2Epred__set_2EFINITE(A_27b),V5P)) & (~~ (V5P = c_2Epred__set_2EEMPTY(A_27b)))))) => (? [V7c:$i] : (mem(V7c,arr(ty_2Enum_2Enum,arr(A_27a,bool))) & (? [V8k:$i] : (mem(V8k,arr(ty_2Enum_2Enum,bool)) & (? [V9z:$i] : (mem(V9z,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) & (p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V0m),f4123(A_27a,A_27b,V1f,V5P)),V8k),V7c),V9z)) & (surj__ty_2Eextreal_2Eextreal(ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V8k),V7c),V9z)) = surj__ty_2Eextreal_2Eextreal(ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27b),f4124(A_27a,A_27b,V3a,V2s,V0m,V4x)),V5P))))))))))))))))))))))))))).
tff(conj_thm_2Elebesgue_2Epsfis__sum,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1f:$i] : (mem(V1f,arr(A_27b,arr(A_27a,ty_2Eextreal_2Eextreal))) => ( ! [V2a:$i] : (mem(V2a,arr(A_27b,ty_2Eextreal_2Eextreal)) => ( ! [V3P:$i] : (mem(V3P,arr(A_27b,bool)) => ((p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & (( ! [V4i:$i] : (mem(V4i,A_27b) => (p(ap(ap(c_2Ebool_2EIN(A_27b),V4i),V3P)) => p(ap(ap(c_2Ebool_2EIN(ty_2Eextreal_2Eextreal),ap(V2a,V4i)),ap(ap(c_2Elebesgue_2Epsfis(A_27a),V0m),ap(V1f,V4i))))))) & p(ap(c_2Epred__set_2EFINITE(A_27b),V3P)))) => p(ap(ap(c_2Ebool_2EIN(ty_2Eextreal_2Eextreal),ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27b),V2a),V3P)),ap(ap(c_2Elebesgue_2Epsfis(A_27a),V0m),f4126(A_27a,A_27b,V1f,V3P))))))))))))))))).
tff(conj_thm_2Elebesgue_2Epsfis__intro,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1a:$i] : (mem(V1a,arr(A_27b,arr(A_27a,bool))) => ( ! [V2x:$i] : (mem(V2x,arr(A_27b,ty_2Erealax_2Ereal)) => ( ! [V3P:$i] : (mem(V3P,arr(A_27b,bool)) => ((p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & (( ! [V4i:$i] : (mem(V4i,A_27b) => (p(ap(ap(c_2Ebool_2EIN(A_27b),V4i),V3P)) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(V1a,V4i)),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m)))))) & (( ! [V5i:$i] : (mem(V5i,A_27b) => (p(ap(ap(c_2Ebool_2EIN(A_27b),V5i),V3P)) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(V2x,V5i)))))) & p(ap(c_2Epred__set_2EFINITE(A_27b),V3P))))) => p(ap(ap(c_2Ebool_2EIN(ty_2Eextreal_2Eextreal),ap(c_2Eextreal_2ENormal,ap(ap(c_2Ereal__sigma_2EREAL__SUM__IMAGE(A_27b),f4127(A_27a,A_27b,V0m,V1a,V2x)),V3P))),ap(ap(c_2Elebesgue_2Epsfis(A_27a),V0m),f4129(A_27a,A_27b,V1a,V2x,V3P))))))))))))))))).
tff(conj_thm_2Elebesgue_2Epos__simple__fn__integral__sub,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ! [V2s:$i] : (mem(V2s,arr(ty_2Enum_2Enum,bool)) => ( ! [V3a:$i] : (mem(V3a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ( ! [V4x:$i] : (mem(V4x,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ( ! [V5g:$i] : (mem(V5g,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ! [V6s_27:$i] : (mem(V6s_27,arr(ty_2Enum_2Enum,bool)) => ( ! [V7b:$i] : (mem(V7b,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ( ! [V8y:$i] : (mem(V8y,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ((p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & (( ! [V9x:$i] : (mem(V9x,A_27a) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(V5g,V9x)),ap(V1f,V9x))))) & (( ! [V10x:$i] : (mem(V10x,A_27a) => (~~ (surj__ty_2Eextreal_2Eextreal(ap(V5g,V10x)) = fo__c_2Eextreal_2EPosInf)))) & (p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V0m),V1f),V2s),V3a),V4x)) & p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V0m),V5g),V6s_27),V7b),V8y)))))) => (? [V11s_27_27:$i] : (mem(V11s_27_27,arr(ty_2Enum_2Enum,bool)) & (? [V12c:$i] : (mem(V12c,arr(ty_2Enum_2Enum,arr(A_27a,bool))) & (? [V13z:$i] : (mem(V13z,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) & (p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V0m),f4130(A_27a,V1f,V5g)),V11s_27_27),V12c),V13z)) & (surj__ty_2Eextreal_2Eextreal(ap(ap(c_2Eextreal_2Eextreal__sub,ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V2s),V3a),V4x)),ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V6s_27),V7b),V8y))) = surj__ty_2Eextreal_2Eextreal(ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V11s_27_27),V12c),V13z)))))))))))))))))))))))))))))))).
tff(conj_thm_2Elebesgue_2Epsfis__sub,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ! [V2g:$i] : (mem(V2g,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ! [V3a:tp__ty_2Eextreal_2Eextreal] : ( ! [V4b:tp__ty_2Eextreal_2Eextreal] : ((p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & (( ! [V5x:$i] : (mem(V5x,A_27a) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(V2g,V5x)),ap(V1f,V5x))))) & (( ! [V6x:$i] : (mem(V6x,A_27a) => (~~ (surj__ty_2Eextreal_2Eextreal(ap(V2g,V6x)) = fo__c_2Eextreal_2EPosInf)))) & (p(ap(ap(c_2Ebool_2EIN(ty_2Eextreal_2Eextreal),inj__ty_2Eextreal_2Eextreal(V3a)),ap(ap(c_2Elebesgue_2Epsfis(A_27a),V0m),V1f))) & p(ap(ap(c_2Ebool_2EIN(ty_2Eextreal_2Eextreal),inj__ty_2Eextreal_2Eextreal(V4b)),ap(ap(c_2Elebesgue_2Epsfis(A_27a),V0m),V2g))))))) => p(ap(ap(c_2Ebool_2EIN(ty_2Eextreal_2Eextreal),ap(ap(c_2Eextreal_2Eextreal__sub,inj__ty_2Eextreal_2Eextreal(V3a)),inj__ty_2Eextreal_2Eextreal(V4b))),ap(ap(c_2Elebesgue_2Epsfis(A_27a),V0m),f4131(A_27a,V1f,V2g)))))))))))))))).
tff(conj_thm_2Elebesgue_2Epos__fn__integral__pos__simple__fn,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ! [V2s:$i] : (mem(V2s,arr(ty_2Enum_2Enum,bool)) => ( ! [V3a:$i] : (mem(V3a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ( ! [V4x:$i] : (mem(V4x,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ((p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V0m),V1f),V2s),V3a),V4x))) => (surj__ty_2Eextreal_2Eextreal(ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),V1f)) = surj__ty_2Eextreal_2Eextreal(ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V2s),V3a),V4x))))))))))))))))).
tff(conj_thm_2Elebesgue_2Epos__fn__integral__mspace,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ((p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & ( ! [V2x:$i] : (mem(V2x,A_27a) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(V1f,V2x)))))) => (surj__ty_2Eextreal_2Eextreal(ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),V1f)) = surj__ty_2Eextreal_2Eextreal(ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),f4132(A_27a,V1f,V0m)))))))))))).
tff(conj_thm_2Elebesgue_2Epos__fn__integral__zero,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => (p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) => (surj__ty_2Eextreal_2Eextreal(ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),k(A_27a,ap(c_2Eextreal_2Eextreal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))) = surj__ty_2Eextreal_2Eextreal(ap(c_2Eextreal_2Eextreal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))))).
tff(conj_thm_2Elebesgue_2Epos__fn__integral__mono,conjecture,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ! [V2g:$i] : (mem(V2g,arr(A_27a,ty_2Eextreal_2Eextreal)) => (( ! [V3x:$i] : (mem(V3x,A_27a) => (p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(V1f,V3x))) & p(ap(ap(c_2Eextreal_2Eextreal__le,ap(V1f,V3x)),ap(V2g,V3x)))))) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),V1f)),ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),V2g))))))))))))).
