include('Axioms/real_topology+2.ax').
fof(mem_c_2Elebesgue_2ERADON__F,axiom,( ! [A_27a] : ( ne(A_27a) => 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)))) ) )).
fof(mem_c_2Elebesgue_2ERADON__F__integrals,axiom,( ! [A_27a] : ( ne(A_27a) => 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)))) ) )).
fof(mem_c_2Elebesgue_2Efinite__space__integral,axiom,( ! [A_27a] : ( ne(A_27a) => 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))) ) )).
fof(mem_c_2Elebesgue_2Efn__seq,axiom,( ! [A_27a] : ( ne(A_27a) => 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))))) ) )).
fof(mem_c_2Elebesgue_2Efn__seq__integral,axiom,( ! [A_27a] : ( ne(A_27a) => 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)))) ) )).
fof(mem_c_2Elebesgue_2Eintegrable,axiom,( ! [A_27a] : ( ne(A_27a) => 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))) ) )).
fof(mem_c_2Elebesgue_2Eintegral,axiom,( ! [A_27a] : ( ne(A_27a) => 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))) ) )).
fof(mem_c_2Elebesgue_2Emax__fn__seq,axiom,( ! [A_27a] : ( ne(A_27a) => 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)))) ) )).
fof(mem_c_2Elebesgue_2Emeasure__absolutely__continuous,axiom,( ! [A_27a] : ( ne(A_27a) => 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))) ) )).
fof(mem_c_2Elebesgue_2Enegative__set,axiom,( ! [A_27a] : ( ne(A_27a) => 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))) ) )).
fof(mem_c_2Elebesgue_2Epos__fn__integral,axiom,( ! [A_27a] : ( ne(A_27a) => 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))) ) )).
fof(mem_c_2Elebesgue_2Epos__simple__fn__integral,axiom,( ! [A_27a] : ( ne(A_27a) => 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))))) ) )).
fof(mem_c_2Elebesgue_2Eprod__measure,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => 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)))) ) ) )).
fof(mem_c_2Elebesgue_2Eprod__measure3,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [A_27c] : ( ne(A_27c) => 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))))) ) ) ) )).
fof(mem_c_2Elebesgue_2Eprod__measure__space,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => 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)))))) ) ) )).
fof(mem_c_2Elebesgue_2Eprod__measure__space3,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [A_27c] : ( ne(A_27c) => 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))))))) ) ) ) )).
fof(mem_c_2Elebesgue_2Eprod__sets3,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [A_27c] : ( ne(A_27c) => 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))))) ) ) ) )).
fof(mem_c_2Elebesgue_2Epsfis,axiom,( ! [A_27a] : ( ne(A_27a) => 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)))) ) )).
fof(mem_c_2Elebesgue_2Epsfs,axiom,( ! [A_27a] : ( ne(A_27a) => 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)))) ) )).
fof(mem_c_2Elebesgue_2Eseq__sup,axiom,( mem(c_2Elebesgue_2Eseq__sup,arr(arr(ty_2Eextreal_2Eextreal,bool),arr(ty_2Enum_2Enum,ty_2Eextreal_2Eextreal))) )).
fof(mem_c_2Elebesgue_2Esigned__measure__space,axiom,( ! [A_27a] : ( ne(A_27a) => 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)) ) )).
fof(ax_thm_2Elebesgue_2Epos__simple__fn__integral__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1s,arr(ty_2Enum_2Enum,bool)) => ! [V2a] : ( mem(V2a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ! [V3x] : ( mem(V3x,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ( ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V1s),V2a),V3x) = ap(c_2Eextreal_2ENormal,ap(ap(c_2Ereal__sigma_2EREAL__SUM__IMAGE(ty_2Enum_2Enum),f4078(A_27a,V0m,V2a,V3x)),V1s)) ) ) ) ) ) ) )).
fof(ax_thm_2Elebesgue_2Epsfs__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0m] : ( 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] : ( 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))) ) ) ) ) )).
fof(ax_thm_2Elebesgue_2Epsfis__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0m] : ( 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] : ( 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)) ) ) ) ) )).
fof(ax_thm_2Elebesgue_2Epos__fn__integral__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),V1f) = ap(c_2Eextreal_2Eextreal__sup,ap(c_2Epred__set_2EGSPEC(ty_2Eextreal_2Eextreal,ty_2Eextreal_2Eextreal),f4087(A_27a,V0m,V1f))) ) ) ) ) )).
fof(ax_thm_2Elebesgue_2Eintegral__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ap(ap(c_2Elebesgue_2Eintegral(A_27a),V0m),V1f) = 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))) ) ) ) ) )).
fof(ax_thm_2Elebesgue_2Eintegrable__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0m] : ( 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] : ( 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))) & ( ( ~~ ( ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),ap(c_2Emeasure_2Efn__plus(A_27a),V1f)) = c_2Eextreal_2EPosInf ) ) & ( ~~ ( ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),ap(c_2Emeasure_2Efn__minus(A_27a),V1f)) = c_2Eextreal_2EPosInf ) ) ) ) ) ) ) ) )).
fof(ax_thm_2Elebesgue_2Efinite__space__integral__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ap(ap(c_2Elebesgue_2Efinite__space__integral(A_27a),V0m),V1f) = 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))) ) ) ) ) )).
fof(ax_thm_2Elebesgue_2Eprod__measure__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0m0] : ( 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] : ( 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) ) ) ) ) ) )).
fof(ax_thm_2Elebesgue_2Eprod__measure__space__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0m0] : ( 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] : ( 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))) ) ) ) ) ) )).
fof(ax_thm_2Elebesgue_2Eprod__sets3__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [A_27c] : ( ne(A_27c) => ! [V0a] : ( mem(V0a,arr(arr(A_27a,bool),bool)) => ! [V1b] : ( mem(V1b,arr(arr(A_27b,bool),bool)) => ! [V2c] : ( 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))) ) ) ) ) ) ) ) )).
fof(ax_thm_2Elebesgue_2Eprod__measure3__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [A_27c] : ( ne(A_27c) => ! [V0m0] : ( 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] : ( 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] : ( 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)) ) ) ) ) ) ) ) )).
fof(ax_thm_2Elebesgue_2Eprod__measure__space3__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [A_27c] : ( ne(A_27c) => ! [V0m0] : ( 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] : ( 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] : ( 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))) ) ) ) ) ) ) ) )).
fof(conj_thm_2Elebesgue_2Epos__simple__fn__integral__present,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2s] : ( mem(V2s,arr(ty_2Enum_2Enum,bool)) => ! [V3a] : ( mem(V3a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ! [V4x] : ( mem(V4x,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ! [V5g] : ( mem(V5g,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V6s_27] : ( mem(V6s_27,arr(ty_2Enum_2Enum,bool)) => ! [V7b] : ( mem(V7b,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ! [V8y] : ( 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] : ( mem(V9z,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) & ? [V10z_27] : ( mem(V10z_27,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) & ? [V11c] : ( mem(V11c,arr(ty_2Enum_2Enum,arr(A_27a,bool))) & ? [V12k] : ( mem(V12k,arr(ty_2Enum_2Enum,bool)) & ( ( ! [V13t] : ( mem(V13t,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V13t),ap(c_2Emeasure_2Em__space(A_27a),V0m))) => ( ap(V1f,V13t) = ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(ty_2Enum_2Enum),f4095(A_27a,V13t,V11c,V9z)),V12k) ) ) ) ) & ( ( ! [V15t] : ( mem(V15t,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V15t),ap(c_2Emeasure_2Em__space(A_27a),V0m))) => ( ap(V5g,V15t) = ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(ty_2Enum_2Enum),f4096(A_27a,V15t,V11c,V10z_27)),V12k) ) ) ) ) & ( ( 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),V12k),V11c),V9z) ) & ( ( ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V6s_27),V7b),V8y) = 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] : ( mem(V17i,ty_2Enum_2Enum) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V17i),V12k)) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),ap(V9z,V17i))) ) ) ) & ( ( ! [V18i] : ( mem(V18i,ty_2Enum_2Enum) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V18i),V12k)) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),ap(V10z_27,V18i))) ) ) ) & ( ( ! [V19i] : ( mem(V19i,ty_2Enum_2Enum) => ! [V20j] : ( mem(V20j,ty_2Enum_2Enum) => ( ( p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V19i),V12k)) & ( p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V20j),V12k)) & ( ~~ ( V19i = V20j ) ) ) ) => p(ap(ap(c_2Epred__set_2EDISJOINT(A_27a),ap(V11c,V19i)),ap(V11c,V20j))) ) ) ) ) & ( ( ! [V21i] : ( mem(V21i,ty_2Enum_2Enum) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V21i),V12k)) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(V11c,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) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Epsfis__present,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2g] : ( mem(V2g,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V3a] : ( mem(V3a,ty_2Eextreal_2Eextreal) => ! [V4b] : ( mem(V4b,ty_2Eextreal_2Eextreal) => ( ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & ( p(ap(ap(c_2Ebool_2EIN(ty_2Eextreal_2Eextreal),V3a),ap(ap(c_2Elebesgue_2Epsfis(A_27a),V0m),V1f))) & p(ap(ap(c_2Ebool_2EIN(ty_2Eextreal_2Eextreal),V4b),ap(ap(c_2Elebesgue_2Epsfis(A_27a),V0m),V2g))) ) ) => ? [V5z] : ( mem(V5z,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) & ? [V6z_27] : ( mem(V6z_27,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) & ? [V7c] : ( mem(V7c,arr(ty_2Enum_2Enum,arr(A_27a,bool))) & ? [V8k] : ( mem(V8k,arr(ty_2Enum_2Enum,bool)) & ( ( ! [V9t] : ( mem(V9t,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V9t),ap(c_2Emeasure_2Em__space(A_27a),V0m))) => ( ap(V1f,V9t) = ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(ty_2Enum_2Enum),f4097(A_27a,V9t,V7c,V5z)),V8k) ) ) ) ) & ( ( ! [V11t] : ( mem(V11t,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V11t),ap(c_2Emeasure_2Em__space(A_27a),V0m))) => ( ap(V2g,V11t) = ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(ty_2Enum_2Enum),f4098(A_27a,V11t,V7c,V6z_27)),V8k) ) ) ) ) & ( ( V3a = ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V8k),V7c),V5z) ) & ( ( V4b = 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] : ( mem(V13i,ty_2Enum_2Enum) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V13i),V8k)) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),ap(V5z,V13i))) ) ) ) & ( ( ! [V14i] : ( mem(V14i,ty_2Enum_2Enum) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V14i),V8k)) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),ap(V6z_27,V14i))) ) ) ) & ( ( ! [V15i] : ( mem(V15i,ty_2Enum_2Enum) => ! [V16j] : ( mem(V16j,ty_2Enum_2Enum) => ( ( p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V15i),V8k)) & ( p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V16j),V8k)) & ( ~~ ( V15i = V16j ) ) ) ) => p(ap(ap(c_2Epred__set_2EDISJOINT(A_27a),ap(V7c,V15i)),ap(V7c,V16j))) ) ) ) ) & ( ( ! [V17i] : ( mem(V17i,ty_2Enum_2Enum) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V17i),V8k)) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(V7c,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) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Epos__simple__fn__thm1,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2s] : ( mem(V2s,arr(ty_2Enum_2Enum,bool)) => ! [V3a] : ( mem(V3a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ! [V4x] : ( mem(V4x,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ! [V5i] : ( mem(V5i,ty_2Enum_2Enum) => ! [V6y] : ( 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),V5i),V2s)) & p(ap(ap(c_2Ebool_2EIN(A_27a),V6y),ap(V3a,V5i))) ) ) ) => ( ap(V1f,V6y) = ap(c_2Eextreal_2ENormal,ap(V4x,V5i)) ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Epos__simple__fn__le,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2g] : ( mem(V2g,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V3s] : ( mem(V3s,arr(ty_2Enum_2Enum,bool)) => ! [V4a] : ( mem(V4a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ! [V5x] : ( mem(V5x,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ! [V6x_27] : ( mem(V6x_27,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ! [V7i] : ( mem(V7i,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] : ( 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),V7i),V3s)) & ( ~~ ( ap(V4a,V7i) = c_2Epred__set_2EEMPTY(A_27a) ) ) ) ) ) ) ) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2ENormal,ap(V6x_27,V7i))),ap(c_2Eextreal_2ENormal,ap(V5x,V7i)))) ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Epos__simple__fn__cmul,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(ty_2Enum_2Enum,bool)) => ! [V1a] : ( mem(V1a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ! [V2x] : ( mem(V2x,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ! [V3m] : ( 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] : ( mem(V4f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V5z] : ( mem(V5z,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,c_2Enum_2E0)),V5z)) ) ) => ? [V6s_27] : ( mem(V6s_27,arr(ty_2Enum_2Enum,bool)) & ? [V7a_27] : ( mem(V7a_27,arr(ty_2Enum_2Enum,arr(A_27a,bool))) & ? [V8x_27] : ( 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)) ) ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Epos__simple__fn__cmul__alt,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2s] : ( mem(V2s,arr(ty_2Enum_2Enum,bool)) => ! [V3a] : ( mem(V3a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ! [V4x] : ( mem(V4x,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ! [V5z] : ( mem(V5z,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,c_2Enum_2E0)),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))) ) ) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Epos__simple__fn__add,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(ty_2Enum_2Enum,bool)) => ! [V1a] : ( mem(V1a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ! [V2x] : ( mem(V2x,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ! [V3s_27] : ( mem(V3s_27,arr(ty_2Enum_2Enum,bool)) => ! [V4a_27] : ( mem(V4a_27,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ! [V5x_27] : ( mem(V5x_27,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ! [V6m] : ( 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] : ( mem(V7f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V8g] : ( 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] : ( mem(V9s_27_27,arr(ty_2Enum_2Enum,bool)) & ? [V10a_27_27] : ( mem(V10a_27_27,arr(ty_2Enum_2Enum,arr(A_27a,bool))) & ? [V11x_27_27] : ( 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)) ) ) ) ) ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Epos__simple__fn__add__alt,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2g] : ( mem(V2g,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V3s] : ( mem(V3s,arr(ty_2Enum_2Enum,bool)) => ! [V4a] : ( mem(V4a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ! [V5x] : ( mem(V5x,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ! [V6y] : ( 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))) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Epos__simple__fn__indicator,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( 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] : ( mem(V2s,arr(ty_2Enum_2Enum,bool)) & ? [V3a] : ( mem(V3a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) & ? [V4x] : ( 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)) ) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Epos__simple__fn__indicator__alt,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( 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),c_2Enum_2E0),ap(ap(c_2Epred__set_2EINSERT(ty_2Enum_2Enum),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))),c_2Epred__set_2EEMPTY(ty_2Enum_2Enum)))),f4105(A_27a,V0m,V1s)),f4106)) ) ) )))).
fof(conj_thm_2Elebesgue_2Epos__simple__fn__max,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0s_27] : ( mem(V0s_27,arr(ty_2Enum_2Enum,bool)) => ! [V1b] : ( mem(V1b,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ! [V2m] : ( 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] : ( mem(V3f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V4s] : ( mem(V4s,arr(ty_2Enum_2Enum,bool)) => ! [V5a] : ( mem(V5a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ! [V6x] : ( mem(V6x,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ! [V7g] : ( mem(V7g,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V8s_27b] : ( mem(V8s_27b,A_27b) => ! [V9y] : ( 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] : ( mem(V10s_27_27,arr(ty_2Enum_2Enum,bool)) & ? [V11a_27_27] : ( mem(V11a_27_27,arr(ty_2Enum_2Enum,arr(A_27a,bool))) & ? [V12x_27_27] : ( 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)) ) ) ) ) ) ) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Elebesgue_2Epos__simple__fn__not__infty,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2s] : ( mem(V2s,arr(ty_2Enum_2Enum,bool)) => ! [V3a] : ( mem(V3a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ! [V4x] : ( 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] : ( mem(V5x,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V5x),ap(c_2Emeasure_2Em__space(A_27a),V0m))) => ( ( ~~ ( ap(V1f,V5x) = c_2Eextreal_2ENegInf ) ) & ( ~~ ( ap(V1f,V5x) = c_2Eextreal_2EPosInf ) ) ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Epos__simple__fn__integral__add,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2s] : ( mem(V2s,arr(ty_2Enum_2Enum,bool)) => ! [V3a] : ( mem(V3a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ! [V4x] : ( mem(V4x,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ! [V5g] : ( mem(V5g,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V6s_27] : ( mem(V6s_27,arr(ty_2Enum_2Enum,bool)) => ! [V7b] : ( mem(V7b,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ! [V8y] : ( 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] : ( mem(V9s_27_27,arr(ty_2Enum_2Enum,bool)) & ? [V10c] : ( mem(V10c,arr(ty_2Enum_2Enum,arr(A_27a,bool))) & ? [V11z] : ( 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)) & ( 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)) = ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V9s_27_27),V10c),V11z) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Epos__simple__fn__integral__add__alt,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2s] : ( mem(V2s,arr(ty_2Enum_2Enum,bool)) => ! [V3a] : ( mem(V3a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ! [V4x] : ( mem(V4x,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ! [V5g] : ( mem(V5g,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V6y] : ( 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)) ) ) => ( 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)) = ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V2s),V3a),f4109(V4x,V6y)) ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Epsfis__add,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2g] : ( mem(V2g,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V3a] : ( mem(V3a,ty_2Eextreal_2Eextreal) => ! [V4b] : ( mem(V4b,ty_2Eextreal_2Eextreal) => ( ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & ( p(ap(ap(c_2Ebool_2EIN(ty_2Eextreal_2Eextreal),V3a),ap(ap(c_2Elebesgue_2Epsfis(A_27a),V0m),V1f))) & p(ap(ap(c_2Ebool_2EIN(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,V3a),V4b)),ap(ap(c_2Elebesgue_2Epsfis(A_27a),V0m),f4110(A_27a,V1f,V2g)))) ) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Epos__simple__fn__integral__mono,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2s] : ( mem(V2s,arr(ty_2Enum_2Enum,bool)) => ! [V3a] : ( mem(V3a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ! [V4x] : ( mem(V4x,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ! [V5g] : ( mem(V5g,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V6s_27] : ( mem(V6s_27,arr(ty_2Enum_2Enum,bool)) => ! [V7b] : ( mem(V7b,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ! [V8y] : ( 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] : ( 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))) ) ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Epsfis__mono,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2g] : ( mem(V2g,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V3a] : ( mem(V3a,ty_2Eextreal_2Eextreal) => ! [V4b] : ( mem(V4b,ty_2Eextreal_2Eextreal) => ( ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & ( p(ap(ap(c_2Ebool_2EIN(ty_2Eextreal_2Eextreal),V3a),ap(ap(c_2Elebesgue_2Epsfis(A_27a),V0m),V1f))) & ( p(ap(ap(c_2Ebool_2EIN(ty_2Eextreal_2Eextreal),V4b),ap(ap(c_2Elebesgue_2Epsfis(A_27a),V0m),V2g))) & ! [V5x] : ( 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,V3a),V4b)) ) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Epos__simple__fn__integral__unique,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2s] : ( mem(V2s,arr(ty_2Enum_2Enum,bool)) => ! [V3a] : ( mem(V3a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ! [V4x] : ( mem(V4x,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ! [V5s_27] : ( mem(V5s_27,arr(ty_2Enum_2Enum,bool)) => ! [V6b] : ( mem(V6b,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ! [V7y] : ( 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)) ) ) => ( 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),V5s_27),V6b),V7y) ) ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Epsfis__unique,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2a] : ( mem(V2a,ty_2Eextreal_2Eextreal) => ! [V3b] : ( mem(V3b,ty_2Eextreal_2Eextreal) => ( ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & ( p(ap(ap(c_2Ebool_2EIN(ty_2Eextreal_2Eextreal),V2a),ap(ap(c_2Elebesgue_2Epsfis(A_27a),V0m),V1f))) & p(ap(ap(c_2Ebool_2EIN(ty_2Eextreal_2Eextreal),V3b),ap(ap(c_2Elebesgue_2Epsfis(A_27a),V0m),V1f))) ) ) => ( V2a = V3b ) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Epos__simple__fn__integral__indicator,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( 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] : ( mem(V2s,arr(ty_2Enum_2Enum,bool)) & ? [V3a] : ( mem(V3a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) & ? [V4x] : ( 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)) & ( ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V2s),V3a),V4x) = ap(c_2Eextreal_2ENormal,ap(ap(c_2Emeasure_2Emeasure(A_27a),V0m),V1A)) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Epsfis__indicator,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( 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)))) ) ) )))).
fof(conj_thm_2Elebesgue_2Epos__simple__fn__integral__cmul,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2s] : ( mem(V2s,arr(ty_2Enum_2Enum,bool)) => ! [V3a] : ( mem(V3a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ! [V4x] : ( mem(V4x,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ! [V5z] : ( mem(V5z,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,c_2Enum_2E0)),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))) & ( ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V2s),V3a),f4112(V4x,V5z)) = ap(ap(c_2Eextreal_2Eextreal__mul,ap(c_2Eextreal_2ENormal,V5z)),ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V2s),V3a),V4x)) ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Epsfis__cmul,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2a] : ( mem(V2a,ty_2Eextreal_2Eextreal) => ! [V3z] : ( mem(V3z,ty_2Erealax_2Ereal) => ( ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & ( p(ap(ap(c_2Ebool_2EIN(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,c_2Enum_2E0)),V3z)) ) ) => p(ap(ap(c_2Ebool_2EIN(ty_2Eextreal_2Eextreal),ap(ap(c_2Eextreal_2Eextreal__mul,ap(c_2Eextreal_2ENormal,V3z)),V2a)),ap(ap(c_2Elebesgue_2Epsfis(A_27a),V0m),f4113(A_27a,V1f,V3z)))) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Epos__simple__fn__integral__cmul__alt,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2s] : ( mem(V2s,arr(ty_2Enum_2Enum,bool)) => ! [V3a] : ( mem(V3a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ! [V4x] : ( mem(V4x,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ! [V5z] : ( mem(V5z,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,c_2Enum_2E0)),V5z)) & p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V0m),V1f),V2s),V3a),V4x)) ) ) => ? [V6s_27] : ( mem(V6s_27,arr(ty_2Enum_2Enum,bool)) & ? [V7a_27] : ( mem(V7a_27,arr(ty_2Enum_2Enum,arr(A_27a,bool))) & ? [V8x_27] : ( 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)) & ( ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V6s_27),V7a_27),V8x_27) = ap(ap(c_2Eextreal_2Eextreal__mul,ap(c_2Eextreal_2ENormal,V5z)),ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V2s),V3a),V4x)) ) ) ) ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2EIN__psfis,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1r,ty_2Eextreal_2Eextreal) => ! [V2f] : ( mem(V2f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Eextreal_2Eextreal),V1r),ap(ap(c_2Elebesgue_2Epsfis(A_27a),V0m),V2f))) => ? [V3s] : ( mem(V3s,arr(ty_2Enum_2Enum,bool)) & ? [V4a] : ( mem(V4a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) & ? [V5x] : ( 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 = ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V3s),V4a),V5x) ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2EIN__psfis__eq,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1r,ty_2Eextreal_2Eextreal) => ! [V2f] : ( mem(V2f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Eextreal_2Eextreal),V1r),ap(ap(c_2Elebesgue_2Epsfis(A_27a),V0m),V2f))) <=> ? [V3s] : ( mem(V3s,arr(ty_2Enum_2Enum,bool)) & ? [V4a] : ( mem(V4a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) & ? [V5x] : ( 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 = ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V3s),V4a),V5x) ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Epsfis__pos,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2a] : ( mem(V2a,ty_2Eextreal_2Eextreal) => ( ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & p(ap(ap(c_2Ebool_2EIN(ty_2Eextreal_2Eextreal),V2a),ap(ap(c_2Elebesgue_2Epsfis(A_27a),V0m),V1f))) ) => ! [V3x] : ( 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,c_2Enum_2E0)),ap(V1f,V3x))) ) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Epos__simple__fn__integral__zero,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1s,arr(ty_2Enum_2Enum,bool)) => ! [V2a] : ( mem(V2a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ! [V3x] : ( 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,c_2Enum_2E0))),V1s),V2a),V3x)) ) => ( ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V1s),V2a),V3x) = ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0) ) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Epos__simple__fn__integral__zero__alt,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0g] : ( mem(V0g,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V1m] : ( 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] : ( mem(V2s,arr(ty_2Enum_2Enum,bool)) => ! [V3a] : ( mem(V3a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ! [V4x] : ( 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] : ( mem(V5x,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V5x),ap(c_2Emeasure_2Em__space(A_27a),V1m))) => ( ap(V0g,V5x) = ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0) ) ) ) ) ) => ( ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V1m),V2s),V3a),V4x) = ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0) ) ) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Epsfis__zero,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1a,ty_2Eextreal_2Eextreal) => ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Eextreal_2Eextreal),V1a),ap(ap(c_2Elebesgue_2Epsfis(A_27a),V0m),k(A_27a,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0))))) <=> ( V1a = ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Epos__simple__fn__integral__not__infty,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1s,arr(ty_2Enum_2Enum,bool)) => ! [V2a] : ( mem(V2a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ! [V3x] : ( mem(V3x,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ( ( ~~ ( ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V1s),V2a),V3x) = c_2Eextreal_2ENegInf ) ) & ( ~~ ( ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V1s),V2a),V3x) = c_2Eextreal_2EPosInf ) ) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Epsfis__not__infty,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2a] : ( mem(V2a,ty_2Eextreal_2Eextreal) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Eextreal_2Eextreal),V2a),ap(ap(c_2Elebesgue_2Epsfis(A_27a),V0m),V1f))) => ( ( ~~ ( V2a = c_2Eextreal_2ENegInf ) ) & ( ~~ ( V2a = c_2Eextreal_2EPosInf ) ) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Epos__simple__fn__integral__sum,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27b,arr(A_27a,ty_2Eextreal_2Eextreal))) => ! [V2s] : ( mem(V2s,arr(ty_2Enum_2Enum,bool)) => ! [V3a] : ( mem(V3a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ! [V4x] : ( mem(V4x,arr(A_27b,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal))) => ! [V5P] : ( mem(V5P,arr(A_27b,bool)) => ( ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & ( ( ! [V6i] : ( 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))) & ( ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V2s),V3a),f4120(A_27b,V4x,V5P)) = ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27b),f4121(A_27a,A_27b,V3a,V0m,V2s,V4x)),V5P) ) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Elebesgue_2Epos__simple__fn__integral__sum__alt,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27b,arr(A_27a,ty_2Eextreal_2Eextreal))) => ! [V2s] : ( mem(V2s,arr(A_27b,arr(ty_2Enum_2Enum,bool))) => ! [V3a] : ( mem(V3a,arr(A_27b,arr(ty_2Enum_2Enum,arr(A_27a,bool)))) => ! [V4x] : ( mem(V4x,arr(A_27b,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal))) => ! [V5P] : ( mem(V5P,arr(A_27b,bool)) => ( ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & ( ( ! [V6i] : ( 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] : ( mem(V7c,arr(ty_2Enum_2Enum,arr(A_27a,bool))) & ? [V8k] : ( mem(V8k,arr(ty_2Enum_2Enum,bool)) & ? [V9z] : ( 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)) & ( ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V8k),V7c),V9z) = ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27b),f4124(A_27a,A_27b,V3a,V2s,V0m,V4x)),V5P) ) ) ) ) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Elebesgue_2Epsfis__sum,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27b,arr(A_27a,ty_2Eextreal_2Eextreal))) => ! [V2a] : ( mem(V2a,arr(A_27b,ty_2Eextreal_2Eextreal)) => ! [V3P] : ( mem(V3P,arr(A_27b,bool)) => ( ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & ( ( ! [V4i] : ( 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)))) ) ) ) ) ))))).
fof(conj_thm_2Elebesgue_2Epsfis__intro,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0m] : ( 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] : ( mem(V1a,arr(A_27b,arr(A_27a,bool))) => ! [V2x] : ( mem(V2x,arr(A_27b,ty_2Erealax_2Ereal)) => ! [V3P] : ( mem(V3P,arr(A_27b,bool)) => ( ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & ( ( ! [V4i] : ( 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] : ( 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,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)))) ) ) ) ) ))))).
fof(conj_thm_2Elebesgue_2Epos__simple__fn__integral__sub,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2s] : ( mem(V2s,arr(ty_2Enum_2Enum,bool)) => ! [V3a] : ( mem(V3a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ! [V4x] : ( mem(V4x,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ! [V5g] : ( mem(V5g,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V6s_27] : ( mem(V6s_27,arr(ty_2Enum_2Enum,bool)) => ! [V7b] : ( mem(V7b,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ! [V8y] : ( mem(V8y,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ( ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & ( ( ! [V9x] : ( mem(V9x,A_27a) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(V5g,V9x)),ap(V1f,V9x))) ) ) & ( ( ! [V10x] : ( mem(V10x,A_27a) => ( ~~ ( ap(V5g,V10x) = 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] : ( mem(V11s_27_27,arr(ty_2Enum_2Enum,bool)) & ? [V12c] : ( mem(V12c,arr(ty_2Enum_2Enum,arr(A_27a,bool))) & ? [V13z] : ( 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)) & ( 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)) = ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V11s_27_27),V12c),V13z) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Epsfis__sub,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2g] : ( mem(V2g,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V3a] : ( mem(V3a,ty_2Eextreal_2Eextreal) => ! [V4b] : ( mem(V4b,ty_2Eextreal_2Eextreal) => ( ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & ( ( ! [V5x] : ( mem(V5x,A_27a) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(V2g,V5x)),ap(V1f,V5x))) ) ) & ( ( ! [V6x] : ( mem(V6x,A_27a) => ( ~~ ( ap(V2g,V6x) = c_2Eextreal_2EPosInf ) ) ) ) & ( p(ap(ap(c_2Ebool_2EIN(ty_2Eextreal_2Eextreal),V3a),ap(ap(c_2Elebesgue_2Epsfis(A_27a),V0m),V1f))) & p(ap(ap(c_2Ebool_2EIN(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,V3a),V4b)),ap(ap(c_2Elebesgue_2Epsfis(A_27a),V0m),f4131(A_27a,V1f,V2g)))) ) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Epos__fn__integral__pos__simple__fn,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2s] : ( mem(V2s,arr(ty_2Enum_2Enum,bool)) => ! [V3a] : ( mem(V3a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ! [V4x] : ( 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)) ) => ( ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),V1f) = ap(ap(ap(ap(c_2Elebesgue_2Epos__simple__fn__integral(A_27a),V0m),V2s),V3a),V4x) ) ) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Epos__fn__integral__mspace,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & ! [V2x] : ( mem(V2x,A_27a) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(V1f,V2x))) ) ) => ( ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),V1f) = ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),f4132(A_27a,V1f,V0m)) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Epos__fn__integral__zero,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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)) => ( ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),k(A_27a,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0))) = ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0) ) ) )))).
fof(conj_thm_2Elebesgue_2Epos__fn__integral__mono,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2g] : ( mem(V2g,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ( ! [V3x] : ( mem(V3x,A_27a) => ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,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))) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Epos__fn__integral__mono__mspace,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2g] : ( mem(V2g,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & ( ( ! [V3x] : ( 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(V2g,V3x)),ap(V1f,V3x))) ) ) ) & ( ( ! [V4x] : ( mem(V4x,A_27a) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(V1f,V4x))) ) ) & ! [V5x] : ( mem(V5x,A_27a) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(V2g,V5x))) ) ) ) ) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),V2g)),ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),V1f))) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Epos__fn__integral__pos,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & ! [V2x] : ( mem(V2x,A_27a) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(V1f,V2x))) ) ) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),V1f))) ) ) )))).
fof(conj_thm_2Elebesgue_2Epos__fn__integral__cmul,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2c] : ( mem(V2c,ty_2Erealax_2Ereal) => ( ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & ( ( ! [V3x] : ( 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,c_2Enum_2E0)),ap(V1f,V3x))) ) ) ) & p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V2c)) ) ) => ( ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),f3441(A_27a,V1f,V2c)) = ap(ap(c_2Eextreal_2Eextreal__mul,ap(c_2Eextreal_2ENormal,V2c)),ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),V1f)) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Epos__fn__integral__indicator,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( 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))) ) => ( ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),ap(c_2Emeasure_2Eindicator__fn(A_27a),V1s)) = ap(c_2Eextreal_2ENormal,ap(ap(c_2Emeasure_2Emeasure(A_27a),V0m),V1s)) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Epos__fn__integral__cmul__indicator,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1s,arr(A_27a,bool)) => ! [V2c] : ( mem(V2c,ty_2Erealax_2Ereal) => ( ( 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(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V2c)) ) ) => ( ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),f4133(A_27a,V1s,V2c)) = ap(c_2Eextreal_2ENormal,ap(ap(c_2Erealax_2Ereal__mul,V2c),ap(ap(c_2Emeasure_2Emeasure(A_27a),V0m),V1s))) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Epos__fn__integral__sum__cmul__indicator,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1s,arr(ty_2Enum_2Enum,bool)) => ! [V2a] : ( mem(V2a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ! [V3x] : ( mem(V3x,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ( ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & ( p(ap(c_2Epred__set_2EFINITE(ty_2Enum_2Enum),V1s)) & ( ( ! [V4i] : ( mem(V4i,ty_2Enum_2Enum) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V4i),V1s)) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),ap(V3x,V4i))) ) ) ) & ! [V5i] : ( mem(V5i,ty_2Enum_2Enum) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V5i),V1s)) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(V2a,V5i)),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m))) ) ) ) ) ) => ( ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),f4135(A_27a,V2a,V3x,V1s)) = ap(c_2Eextreal_2ENormal,ap(ap(c_2Ereal__sigma_2EREAL__SUM__IMAGE(ty_2Enum_2Enum),f4136(A_27a,V0m,V2a,V3x)),V1s)) ) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Elebesgue__monotone__convergence__lemma,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2fi] : ( mem(V2fi,arr(ty_2Enum_2Enum,arr(A_27a,ty_2Eextreal_2Eextreal))) => ! [V3g] : ( mem(V3g,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V4r_27] : ( mem(V4r_27,ty_2Eextreal_2Eextreal) => ( ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & ( ( ! [V5i] : ( mem(V5i,ty_2Enum_2Enum) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,ty_2Eextreal_2Eextreal)),ap(V2fi,V5i)),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))) ) ) & ( ( ! [V6x] : ( mem(V6x,A_27a) => p(ap(c_2Eextreal_2Eext__mono__increasing,f4137(A_27a,V2fi,V6x))) ) ) & ( ( ! [V8x] : ( mem(V8x,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V8x),ap(c_2Emeasure_2Em__space(A_27a),V0m))) => ( ap(c_2Eextreal_2Eextreal__sup,ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,ty_2Eextreal_2Eextreal),f4138(A_27a,V2fi,V8x)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum))) = ap(V1f,V8x) ) ) ) ) & ( p(ap(ap(c_2Ebool_2EIN(ty_2Eextreal_2Eextreal),V4r_27),ap(ap(c_2Elebesgue_2Epsfis(A_27a),V0m),V3g))) & ( ( ! [V10x] : ( mem(V10x,A_27a) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(V3g,V10x)),ap(V1f,V10x))) ) ) & ! [V11i] : ( mem(V11i,ty_2Enum_2Enum) => ! [V12x] : ( mem(V12x,A_27a) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(ap(V2fi,V11i),V12x))) ) ) ) ) ) ) ) ) => p(ap(ap(c_2Eextreal_2Eextreal__le,V4r_27),ap(c_2Eextreal_2Eextreal__sup,ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,ty_2Eextreal_2Eextreal),f4139(A_27a,V2fi,V0m)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum))))) ) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Elebesgue__monotone__convergence,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2fi] : ( mem(V2fi,arr(ty_2Enum_2Enum,arr(A_27a,ty_2Eextreal_2Eextreal))) => ( ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & ( ( ! [V3i] : ( mem(V3i,ty_2Enum_2Enum) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,ty_2Eextreal_2Eextreal)),ap(V2fi,V3i)),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))) ) ) & ( ( ! [V4i] : ( mem(V4i,ty_2Enum_2Enum) => ! [V5x] : ( mem(V5x,A_27a) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(ap(V2fi,V4i),V5x))) ) ) ) & ( ( ! [V6x] : ( mem(V6x,A_27a) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(V1f,V6x))) ) ) & ( ( ! [V7x] : ( mem(V7x,A_27a) => p(ap(c_2Eextreal_2Eext__mono__increasing,f4140(A_27a,V2fi,V7x))) ) ) & ! [V9x] : ( mem(V9x,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V9x),ap(c_2Emeasure_2Em__space(A_27a),V0m))) => ( ap(c_2Eextreal_2Eextreal__sup,ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,ty_2Eextreal_2Eextreal),f4141(A_27a,V2fi,V9x)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum))) = ap(V1f,V9x) ) ) ) ) ) ) ) ) => ( ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),V1f) = ap(c_2Eextreal_2Eextreal__sup,ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,ty_2Eextreal_2Eextreal),f4142(A_27a,V2fi,V0m)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum))) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Elebesgue__monotone__convergence__subset,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2fi] : ( mem(V2fi,arr(ty_2Enum_2Enum,arr(A_27a,ty_2Eextreal_2Eextreal))) => ! [V3A] : ( mem(V3A,arr(A_27a,bool)) => ( ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & ( ( ! [V4i] : ( mem(V4i,ty_2Enum_2Enum) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,ty_2Eextreal_2Eextreal)),ap(V2fi,V4i)),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))) ) ) & ( ( ! [V5i] : ( mem(V5i,ty_2Enum_2Enum) => ! [V6x] : ( mem(V6x,A_27a) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(ap(V2fi,V5i),V6x))) ) ) ) & ( ( ! [V7x] : ( mem(V7x,A_27a) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(V1f,V7x))) ) ) & ( ( ! [V8x] : ( mem(V8x,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V8x),ap(c_2Emeasure_2Em__space(A_27a),V0m))) => ( ap(c_2Eextreal_2Eextreal__sup,ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,ty_2Eextreal_2Eextreal),f4138(A_27a,V2fi,V8x)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum))) = ap(V1f,V8x) ) ) ) ) & ( ( ! [V10x] : ( mem(V10x,A_27a) => p(ap(c_2Eextreal_2Eext__mono__increasing,f4143(A_27a,V2fi,V10x))) ) ) & p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V3A),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m))) ) ) ) ) ) ) => ( ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),f4144(A_27a,V1f,V3A)) = ap(c_2Eextreal_2Eextreal__sup,ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,ty_2Eextreal_2Eextreal),f4146(A_27a,V3A,V2fi,V0m)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum))) ) ) ) ) ) )))).
fof(ax_thm_2Elebesgue_2Efn__seq__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ap(ap(c_2Elebesgue_2Efn__seq(A_27a),V0m),V1f) = f4151(A_27a,V0m,V1f) ) ) ) ) )).
fof(ax_thm_2Elebesgue_2Efn__seq__integral__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ap(ap(c_2Elebesgue_2Efn__seq__integral(A_27a),V0m),V1f) = f4155(A_27a,V1f,V0m) ) ) ) ) )).
fof(conj_thm_2Elebesgue_2Elemma__fn__1,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ! [V3x] : ( mem(V3x,A_27a) => ! [V4k] : ( mem(V4k,ty_2Enum_2Enum) => ( ( p(ap(ap(c_2Ebool_2EIN(A_27a),V3x),ap(c_2Emeasure_2Em__space(A_27a),V0m))) & ( p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V4k),ap(c_2Epred__set_2Ecount,ap(ap(c_2Earithmetic_2EEXP,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),V2n)))) & ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__div,ap(c_2Eextreal_2Eextreal__of__num,V4k)),ap(ap(c_2Eextreal_2Eextreal__pow,ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),V2n))),ap(V1f,V3x))) & p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(V1f,V3x)),ap(ap(c_2Eextreal_2Eextreal__div,ap(ap(c_2Eextreal_2Eextreal__add,ap(c_2Eextreal_2Eextreal__of__num,V4k)),ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),ap(ap(c_2Eextreal_2Eextreal__pow,ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),V2n)))) ) ) ) => ( ap(ap(ap(ap(c_2Elebesgue_2Efn__seq(A_27a),V0m),V1f),V2n),V3x) = ap(ap(c_2Eextreal_2Eextreal__div,ap(c_2Eextreal_2Eextreal__of__num,V4k)),ap(ap(c_2Eextreal_2Eextreal__pow,ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),V2n)) ) ) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Elemma__fn__2,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ! [V3x] : ( 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(ap(c_2Eextreal_2Eextreal__pow,ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),V2n)),ap(V1f,V3x))) ) => ( ap(ap(ap(ap(c_2Elebesgue_2Efn__seq(A_27a),V0m),V1f),V2n),V3x) = ap(ap(c_2Eextreal_2Eextreal__pow,ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),V2n) ) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Elemma__fn__3,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ! [V3x] : ( 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,c_2Enum_2E0)),ap(V1f,V3x))) ) => ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__pow,ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),V2n)),ap(V1f,V3x))) | ? [V4k] : ( mem(V4k,ty_2Enum_2Enum) & ( p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V4k),ap(c_2Epred__set_2Ecount,ap(ap(c_2Earithmetic_2EEXP,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),V2n)))) & ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__div,ap(c_2Eextreal_2Eextreal__of__num,V4k)),ap(ap(c_2Eextreal_2Eextreal__pow,ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),V2n))),ap(V1f,V3x))) & p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(V1f,V3x)),ap(ap(c_2Eextreal_2Eextreal__div,ap(ap(c_2Eextreal_2Eextreal__add,ap(c_2Eextreal_2Eextreal__of__num,V4k)),ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),ap(ap(c_2Eextreal_2Eextreal__pow,ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),V2n)))) ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Elemma__fn__4,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ! [V3x] : ( mem(V3x,A_27a) => ( ( ~~ p(ap(ap(c_2Ebool_2EIN(A_27a),V3x),ap(c_2Emeasure_2Em__space(A_27a),V0m))) ) => ( ap(ap(ap(ap(c_2Elebesgue_2Efn__seq(A_27a),V0m),V1f),V2n),V3x) = ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0) ) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Elemma__fn__5,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ! [V3x] : ( mem(V3x,A_27a) => ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(V1f,V3x))) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(ap(ap(ap(c_2Elebesgue_2Efn__seq(A_27a),V0m),V1f),V2n),V3x))) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Elemma__fn__mono__increasing,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2x] : ( mem(V2x,A_27a) => ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(V1f,V2x))) => p(ap(c_2Eextreal_2Eext__mono__increasing,f4156(A_27a,V0m,V1f,V2x))) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Elemma__fn__upper__bounded,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ! [V3x] : ( mem(V3x,A_27a) => ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(V1f,V3x))) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(ap(ap(c_2Elebesgue_2Efn__seq(A_27a),V0m),V1f),V2n),V3x)),ap(V1f,V3x))) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Elemma__fn__sup,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2x] : ( mem(V2x,A_27a) => ( ( p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),ap(c_2Emeasure_2Em__space(A_27a),V0m))) & p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(V1f,V2x))) ) => ( ap(c_2Eextreal_2Eextreal__sup,ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,ty_2Eextreal_2Eextreal),f4156(A_27a,V0m,V1f,V2x)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum))) = ap(V1f,V2x) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Elemma__fn__in__psfis,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ( ( ( ! [V3x] : ( mem(V3x,A_27a) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(V1f,V3x))) ) ) & ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & 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))) ) ) => p(ap(ap(c_2Ebool_2EIN(ty_2Eextreal_2Eextreal),ap(ap(ap(c_2Elebesgue_2Efn__seq__integral(A_27a),V0m),V1f),V2n)),ap(ap(c_2Elebesgue_2Epsfis(A_27a),V0m),ap(ap(ap(c_2Elebesgue_2Efn__seq(A_27a),V0m),V1f),V2n)))) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Eintegral__sequence,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ( ( ! [V2x] : ( mem(V2x,A_27a) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(V1f,V2x))) ) ) & ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & 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))) ) ) => ( ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),V1f) = ap(c_2Eextreal_2Eextreal__sup,ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,ty_2Eextreal_2Eextreal),f4157(A_27a,V1f,V0m)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum))) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Emeasurable__sequence,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & 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))) ) => ( ( ? [V2fi] : ( mem(V2fi,arr(ty_2Enum_2Enum,arr(A_27a,ty_2Eextreal_2Eextreal))) & ? [V3ri] : ( mem(V3ri,arr(ty_2Enum_2Enum,ty_2Eextreal_2Eextreal)) & ( ( ! [V4x] : ( mem(V4x,A_27a) => p(ap(c_2Eextreal_2Eext__mono__increasing,f4158(A_27a,V2fi,V4x))) ) ) & ( ( ! [V6x] : ( mem(V6x,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V6x),ap(c_2Emeasure_2Em__space(A_27a),V0m))) => ( ap(c_2Eextreal_2Eextreal__sup,ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,ty_2Eextreal_2Eextreal),f4137(A_27a,V2fi,V6x)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum))) = ap(ap(c_2Emeasure_2Efn__plus(A_27a),V1f),V6x) ) ) ) ) & ( ( ! [V8i] : ( mem(V8i,ty_2Enum_2Enum) => p(ap(ap(c_2Ebool_2EIN(ty_2Eextreal_2Eextreal),ap(V3ri,V8i)),ap(ap(c_2Elebesgue_2Epsfis(A_27a),V0m),ap(V2fi,V8i)))) ) ) & ( ( ! [V9i] : ( mem(V9i,ty_2Enum_2Enum) => ! [V10x] : ( mem(V10x,A_27a) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(V2fi,V9i),V10x)),ap(ap(c_2Emeasure_2Efn__plus(A_27a),V1f),V10x))) ) ) ) & ( ( ! [V11i] : ( mem(V11i,ty_2Enum_2Enum) => ! [V12x] : ( mem(V12x,A_27a) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(ap(V2fi,V11i),V12x))) ) ) ) & ( ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),ap(c_2Emeasure_2Efn__plus(A_27a),V1f)) = ap(c_2Eextreal_2Eextreal__sup,ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,ty_2Eextreal_2Eextreal),f4139(A_27a,V2fi,V0m)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum))) ) ) ) ) ) ) ) ) ) & ? [V14gi] : ( mem(V14gi,arr(ty_2Enum_2Enum,arr(A_27a,ty_2Eextreal_2Eextreal))) & ? [V15vi] : ( mem(V15vi,arr(ty_2Enum_2Enum,ty_2Eextreal_2Eextreal)) & ( ( ! [V16x] : ( mem(V16x,A_27a) => p(ap(c_2Eextreal_2Eext__mono__increasing,f4159(A_27a,V14gi,V16x))) ) ) & ( ( ! [V18x] : ( mem(V18x,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V18x),ap(c_2Emeasure_2Em__space(A_27a),V0m))) => ( ap(c_2Eextreal_2Eextreal__sup,ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,ty_2Eextreal_2Eextreal),f4160(A_27a,V14gi,V18x)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum))) = ap(ap(c_2Emeasure_2Efn__minus(A_27a),V1f),V18x) ) ) ) ) & ( ( ! [V20i] : ( mem(V20i,ty_2Enum_2Enum) => p(ap(ap(c_2Ebool_2EIN(ty_2Eextreal_2Eextreal),ap(V15vi,V20i)),ap(ap(c_2Elebesgue_2Epsfis(A_27a),V0m),ap(V14gi,V20i)))) ) ) & ( ( ! [V21i] : ( mem(V21i,ty_2Enum_2Enum) => ! [V22x] : ( mem(V22x,A_27a) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(V14gi,V21i),V22x)),ap(ap(c_2Emeasure_2Efn__minus(A_27a),V1f),V22x))) ) ) ) & ( ( ! [V23i] : ( mem(V23i,ty_2Enum_2Enum) => ! [V24x] : ( mem(V24x,A_27a) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(ap(V14gi,V23i),V24x))) ) ) ) & ( ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),ap(c_2Emeasure_2Efn__minus(A_27a),V1f)) = ap(c_2Eextreal_2Eextreal__sup,ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,ty_2Eextreal_2Eextreal),f4161(A_27a,V14gi,V0m)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum))) ) ) ) ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Epos__fn__integral__add,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2g] : ( mem(V2g,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & ( ( ! [V3x] : ( mem(V3x,A_27a) => ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(V1f,V3x))) & p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(V2g,V3x))) ) ) ) & ( 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))) & p(ap(ap(c_2Ebool_2EIN(arr(A_27a,ty_2Eextreal_2Eextreal)),V2g),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))) ) ) ) => ( ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),f4162(A_27a,V1f,V2g)) = ap(ap(c_2Eextreal_2Eextreal__add,ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),V1f)),ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),V2g)) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Epos__fn__integral__sum,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27b,arr(A_27a,ty_2Eextreal_2Eextreal))) => ! [V2s] : ( mem(V2s,arr(A_27b,bool)) => ( ( p(ap(c_2Epred__set_2EFINITE(A_27b),V2s)) & ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & ( ( ! [V3i] : ( mem(V3i,A_27b) => ( p(ap(ap(c_2Ebool_2EIN(A_27b),V3i),V2s)) => ! [V4x] : ( mem(V4x,A_27a) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(ap(V1f,V3i),V4x))) ) ) ) ) & ! [V5i] : ( mem(V5i,A_27b) => ( p(ap(ap(c_2Ebool_2EIN(A_27b),V5i),V2s)) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,ty_2Eextreal_2Eextreal)),ap(V1f,V5i)),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))) ) ) ) ) ) => ( ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),f4164(A_27a,A_27b,V1f,V2s)) = ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27b),f4165(A_27b,A_27a,V1f,V0m)),V2s) ) ) ) ) ))))).
fof(conj_thm_2Elebesgue_2Epos__fn__integral__disjoint__sets,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2s] : ( mem(V2s,arr(A_27a,bool)) => ! [V3t] : ( mem(V3t,arr(A_27a,bool)) => ( ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & ( p(ap(ap(c_2Epred__set_2EDISJOINT(A_27a),V2s),V3t)) & ( p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V2s),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m))) & ( p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V3t),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m))) & ( 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))) & ! [V4x] : ( mem(V4x,A_27a) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(V1f,V4x))) ) ) ) ) ) ) => ( ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),f4166(A_27a,V3t,V2s,V1f)) = ap(ap(c_2Eextreal_2Eextreal__add,ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),f4167(A_27a,V1f,V2s))),ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),f4168(A_27a,V1f,V3t))) ) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Epos__fn__integral__disjoint__sets__sum,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2s] : ( mem(V2s,arr(A_27b,bool)) => ! [V3a] : ( mem(V3a,arr(A_27b,arr(A_27a,bool))) => ( ( p(ap(c_2Epred__set_2EFINITE(A_27b),V2s)) & ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & ( ( ! [V4i] : ( mem(V4i,A_27b) => ( p(ap(ap(c_2Ebool_2EIN(A_27b),V4i),V2s)) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(V3a,V4i)),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m))) ) ) ) & ( ( ! [V5x] : ( mem(V5x,A_27a) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(V1f,V5x))) ) ) & ( ( ! [V6i] : ( mem(V6i,A_27b) => ! [V7j] : ( mem(V7j,A_27b) => ( ( p(ap(ap(c_2Ebool_2EIN(A_27b),V6i),V2s)) & ( p(ap(ap(c_2Ebool_2EIN(A_27b),V7j),V2s)) & ( ~~ ( V6i = V7j ) ) ) ) => p(ap(ap(c_2Epred__set_2EDISJOINT(A_27a),ap(V3a,V6i)),ap(V3a,V7j))) ) ) ) ) & 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))) ) ) ) ) ) => ( ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),f4169(A_27b,A_27a,V3a,V2s,V1f)) = ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27b),f4171(A_27b,A_27a,V1f,V3a,V0m)),V2s) ) ) ) ) ) ))))).
fof(conj_thm_2Elebesgue_2Epos__fn__integral__split,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2s] : ( mem(V2s,arr(A_27a,bool)) => ( ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & ( p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V2s),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m))) & ( ( ! [V3x] : ( mem(V3x,A_27a) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(V1f,V3x))) ) ) & 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))) ) ) ) => ( ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),V1f) = ap(ap(c_2Eextreal_2Eextreal__add,ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),f4172(A_27a,V1f,V2s))),ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),f4173(A_27a,V2s,V0m,V1f))) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Epos__fn__integral__cmul__infty,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( 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))) ) => ( ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),f4174(A_27a,V1s)) = ap(ap(c_2Eextreal_2Eextreal__mul,c_2Eextreal_2EPosInf),ap(c_2Eextreal_2ENormal,ap(ap(c_2Emeasure_2Emeasure(A_27a),V0m),V1s))) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Epos__fn__integral__suminf,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(ty_2Enum_2Enum,arr(A_27a,ty_2Eextreal_2Eextreal))) => ( ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & ( ( ! [V2i] : ( mem(V2i,ty_2Enum_2Enum) => ! [V3x] : ( mem(V3x,A_27a) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(ap(V1f,V2i),V3x))) ) ) ) & ! [V4i] : ( mem(V4i,ty_2Enum_2Enum) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,ty_2Eextreal_2Eextreal)),ap(V1f,V4i)),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))) ) ) ) => ( ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),f4176(A_27a,V1f)) = ap(c_2Eextreal_2Eext__suminf,f4177(A_27a,V1f,V0m)) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Eintegral__pos__fn,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & ! [V2x] : ( mem(V2x,A_27a) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(V1f,V2x))) ) ) => ( ap(ap(c_2Elebesgue_2Eintegral(A_27a),V0m),V1f) = ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),V1f) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Eintegrable__pos,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & ! [V2x] : ( mem(V2x,A_27a) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(V1f,V2x))) ) ) => ( 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))) & ( ~~ ( ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),V1f) = c_2Eextreal_2EPosInf ) ) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Eintegrable__infty,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2s] : ( mem(V2s,arr(A_27a,bool)) => ( ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & ( p(ap(ap(c_2Elebesgue_2Eintegrable(A_27a),V0m),V1f)) & ( p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V2s),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m))) & ! [V3x] : ( mem(V3x,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V3x),V2s)) => ( ap(V1f,V3x) = c_2Eextreal_2EPosInf ) ) ) ) ) ) => ( ap(ap(c_2Emeasure_2Emeasure(A_27a),V0m),V2s) = ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Eintegrable__infty__null,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & p(ap(ap(c_2Elebesgue_2Eintegrable(A_27a),V0m),V1f)) ) => p(ap(ap(c_2Emeasure_2Enull__set(A_27a),V0m),ap(c_2Epred__set_2EGSPEC(A_27a,A_27a),f4178(A_27a,V1f,V0m)))) ) ) )))).
fof(conj_thm_2Elebesgue_2Eintegrable__bounded,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2g] : ( mem(V2g,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & ( p(ap(ap(c_2Elebesgue_2Eintegrable(A_27a),V0m),V1f)) & ( p(ap(ap(c_2Ebool_2EIN(arr(A_27a,ty_2Eextreal_2Eextreal)),V2g),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))) & ! [V3x] : ( mem(V3x,A_27a) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__abs,ap(V2g,V3x))),ap(V1f,V3x))) ) ) ) ) => p(ap(ap(c_2Elebesgue_2Eintegrable(A_27a),V0m),V2g)) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Eintegrable__fn__plus,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & p(ap(ap(c_2Elebesgue_2Eintegrable(A_27a),V0m),V1f)) ) => p(ap(ap(c_2Elebesgue_2Eintegrable(A_27a),V0m),ap(c_2Emeasure_2Efn__plus(A_27a),V1f))) ) ) )))).
fof(conj_thm_2Elebesgue_2Eintegrable__fn__minus,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & p(ap(ap(c_2Elebesgue_2Eintegrable(A_27a),V0m),V1f)) ) => p(ap(ap(c_2Elebesgue_2Eintegrable(A_27a),V0m),ap(c_2Emeasure_2Efn__minus(A_27a),V1f))) ) ) )))).
fof(conj_thm_2Elebesgue_2Eintegrable__const,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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)))) => ! [V1c] : ( mem(V1c,ty_2Erealax_2Ereal) => ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) => p(ap(ap(c_2Elebesgue_2Eintegrable(A_27a),V0m),k(A_27a,ap(c_2Eextreal_2ENormal,V1c)))) ) ) )))).
fof(conj_thm_2Elebesgue_2Eintegrable__zero,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0m] : ( 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)))) => ! [V1c] : ( mem(V1c,A_27b) => ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) => p(ap(ap(c_2Elebesgue_2Eintegrable(A_27a),V0m),k(A_27a,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)))) ) ) ))))).
fof(conj_thm_2Elebesgue_2Eintegrable__plus__minus,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) => ( 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))) & ( p(ap(ap(c_2Elebesgue_2Eintegrable(A_27a),V0m),ap(c_2Emeasure_2Efn__plus(A_27a),V1f))) & p(ap(ap(c_2Elebesgue_2Eintegrable(A_27a),V0m),ap(c_2Emeasure_2Efn__minus(A_27a),V1f))) ) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Eintegrable__add__pos,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2g] : ( mem(V2g,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & ( p(ap(ap(c_2Elebesgue_2Eintegrable(A_27a),V0m),V1f)) & ( p(ap(ap(c_2Elebesgue_2Eintegrable(A_27a),V0m),V2g)) & ( ( ! [V3x] : ( mem(V3x,A_27a) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(V1f,V3x))) ) ) & ! [V4x] : ( mem(V4x,A_27a) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(V2g,V4x))) ) ) ) ) ) => p(ap(ap(c_2Elebesgue_2Eintegrable(A_27a),V0m),f4110(A_27a,V1f,V2g))) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Eintegrable__add__lemma,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2g] : ( mem(V2g,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & ( p(ap(ap(c_2Elebesgue_2Eintegrable(A_27a),V0m),V1f)) & p(ap(ap(c_2Elebesgue_2Eintegrable(A_27a),V0m),V2g)) ) ) => ( p(ap(ap(c_2Elebesgue_2Eintegrable(A_27a),V0m),f4179(A_27a,V1f,V2g))) & p(ap(ap(c_2Elebesgue_2Eintegrable(A_27a),V0m),f4180(A_27a,V1f,V2g))) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Eintegrable__add,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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)))) => ! [V1f1] : ( mem(V1f1,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2f2] : ( mem(V2f2,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & ( p(ap(ap(c_2Elebesgue_2Eintegrable(A_27a),V0m),V1f1)) & p(ap(ap(c_2Elebesgue_2Eintegrable(A_27a),V0m),V2f2)) ) ) => p(ap(ap(c_2Elebesgue_2Eintegrable(A_27a),V0m),f4181(A_27a,V1f1,V2f2))) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Eintegrable__cmul,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2c] : ( mem(V2c,ty_2Erealax_2Ereal) => ( ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & p(ap(ap(c_2Elebesgue_2Eintegrable(A_27a),V0m),V1f)) ) => p(ap(ap(c_2Elebesgue_2Eintegrable(A_27a),V0m),f4182(A_27a,V1f,V2c))) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Eintegrable__sub,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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)))) => ! [V1f1] : ( mem(V1f1,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2f2] : ( mem(V2f2,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & ( p(ap(ap(c_2Elebesgue_2Eintegrable(A_27a),V0m),V1f1)) & p(ap(ap(c_2Elebesgue_2Eintegrable(A_27a),V0m),V2f2)) ) ) => p(ap(ap(c_2Elebesgue_2Eintegrable(A_27a),V0m),f4183(A_27a,V1f1,V2f2))) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Eintegrable__indicator,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( 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(c_2Elebesgue_2Eintegrable(A_27a),V0m),ap(c_2Emeasure_2Eindicator__fn(A_27a),V1s))) ) ) )))).
fof(conj_thm_2Elebesgue_2Eintegrable__not__infty,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & ( p(ap(ap(c_2Elebesgue_2Eintegrable(A_27a),V0m),V1f)) & ! [V2x] : ( mem(V2x,A_27a) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(V1f,V2x))) ) ) ) => ? [V3g] : ( mem(V3g,arr(A_27a,ty_2Eextreal_2Eextreal)) & ( p(ap(ap(c_2Elebesgue_2Eintegrable(A_27a),V0m),V3g)) & ( ( ! [V4x] : ( mem(V4x,A_27a) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(V3g,V4x))) ) ) & ( ( ! [V5x] : ( mem(V5x,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V5x),ap(c_2Emeasure_2Em__space(A_27a),V0m))) => ( ~~ ( ap(V3g,V5x) = c_2Eextreal_2EPosInf ) ) ) ) ) & ( ap(ap(c_2Elebesgue_2Eintegral(A_27a),V0m),V1f) = ap(ap(c_2Elebesgue_2Eintegral(A_27a),V0m),V3g) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Eintegrable__not__infty__alt,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & ( p(ap(ap(c_2Elebesgue_2Eintegrable(A_27a),V0m),V1f)) & ! [V2x] : ( mem(V2x,A_27a) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(V1f,V2x))) ) ) ) => ( p(ap(ap(c_2Elebesgue_2Eintegrable(A_27a),V0m),f4184(A_27a,V1f))) & ( ap(ap(c_2Elebesgue_2Eintegral(A_27a),V0m),V1f) = ap(ap(c_2Elebesgue_2Eintegral(A_27a),V0m),f4185(A_27a,V1f)) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Eintegrable__not__infty__alt2,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & ( p(ap(ap(c_2Elebesgue_2Eintegrable(A_27a),V0m),V1f)) & ! [V2x] : ( mem(V2x,A_27a) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(V1f,V2x))) ) ) ) => ( p(ap(ap(c_2Elebesgue_2Eintegrable(A_27a),V0m),f4184(A_27a,V1f))) & ( ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),V1f) = ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),f4185(A_27a,V1f)) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Eintegrable__not__infty__alt3,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & p(ap(ap(c_2Elebesgue_2Eintegrable(A_27a),V0m),V1f)) ) => ( p(ap(ap(c_2Elebesgue_2Eintegrable(A_27a),V0m),f4186(A_27a,V1f))) & ( ap(ap(c_2Elebesgue_2Eintegral(A_27a),V0m),V1f) = ap(ap(c_2Elebesgue_2Eintegral(A_27a),V0m),f4187(A_27a,V1f)) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Eintegral__indicator,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( 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))) ) => ( ap(ap(c_2Elebesgue_2Eintegral(A_27a),V0m),ap(c_2Emeasure_2Eindicator__fn(A_27a),V1s)) = ap(c_2Eextreal_2ENormal,ap(ap(c_2Emeasure_2Emeasure(A_27a),V0m),V1s)) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Eintegral__add__lemma,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2f1] : ( mem(V2f1,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V3f2] : ( mem(V3f2,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & ( p(ap(ap(c_2Elebesgue_2Eintegrable(A_27a),V0m),V1f)) & ( p(ap(ap(c_2Elebesgue_2Eintegrable(A_27a),V0m),V2f1)) & ( p(ap(ap(c_2Elebesgue_2Eintegrable(A_27a),V0m),V3f2)) & ( ( V1f = f4188(A_27a,V2f1,V3f2) ) & ( ( ! [V5x] : ( mem(V5x,A_27a) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(V2f1,V5x))) ) ) & ! [V6x] : ( mem(V6x,A_27a) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(V3f2,V6x))) ) ) ) ) ) ) ) => ( ap(ap(c_2Elebesgue_2Eintegral(A_27a),V0m),V1f) = ap(ap(c_2Eextreal_2Eextreal__sub,ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),V2f1)),ap(ap(c_2Elebesgue_2Epos__fn__integral(A_27a),V0m),V3f2)) ) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Eintegral__add,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2g] : ( mem(V2g,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & ( p(ap(ap(c_2Elebesgue_2Eintegrable(A_27a),V0m),V1f)) & p(ap(ap(c_2Elebesgue_2Eintegrable(A_27a),V0m),V2g)) ) ) => ( ap(ap(c_2Elebesgue_2Eintegral(A_27a),V0m),f4189(A_27a,V1f,V2g)) = ap(ap(c_2Eextreal_2Eextreal__add,ap(ap(c_2Elebesgue_2Eintegral(A_27a),V0m),V1f)),ap(ap(c_2Elebesgue_2Eintegral(A_27a),V0m),V2g)) ) ) ) ) )))).
fof(conj_thm_2Elebesgue_2Eintegral__cmul,conjecture,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( 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] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2c] : ( mem(V2c,ty_2Erealax_2Ereal) => ( ( p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & p(ap(ap(c_2Elebesgue_2Eintegrable(A_27a),V0m),V1f)) ) => ( ap(ap(c_2Elebesgue_2Eintegral(A_27a),V0m),f4182(A_27a,V1f,V2c)) = ap(ap(c_2Eextreal_2Eextreal__mul,ap(c_2Eextreal_2ENormal,V2c)),ap(ap(c_2Elebesgue_2Eintegral(A_27a),V0m),V1f)) ) ) ) ) )))).
