Definitions of modes:

1.
MIDSP_2

definition
 mode Group_with_the_operator_« is Group_with_the_operator_«-like AbGroup;
end;
*** change for:  midpoint_operator AbGroup
Group_with_the_operator_« has been removed from MML

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

2.

definition
 let L1, L2 be Lattice;
 mode Ú¿-Homomorphism of L1,L2 ->
 Function of the carrier of L1, the carrier of L2 means
:: VECTSP_8: def 8
   for a, b being Element of the carrier of L1 holds
                              it.(a Ú¿ b) = it.a Ú¿ it.b;
end;
*** change for:  Semilattice-Homomorphism

definition
 let L1, L2 being Lattice;
 mode ÀÙ-Homomorphism of L1, L2 ->
 Function of the carrier of L1, the carrier of L2  means
:: VECTSP_8: def 9
    for a, b being Element of the carrier of L1 holds
                              it.(a ÀÙ b) = it.a ÀÙ it.b;
end;
*** change for:  sup-Semilattice-Homomorphism

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

3.

definition  :: à jest 224
  let T be non empty TopSpace;
    mode à-set of T -> Subset of the carrier of T means
:: DECOMP_1: def 1
   it c= Int Cl Int it;
end;
*** change for:  alpha-set

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

4.

definition
   let X be set;
   mode å_Field_Subset of X is å_Field_Subset-like Dom_set_fam of X;
end;
*** change for:  sigma_Field_Subset

definition
   let X be set;
   let S be å_Field_Subset of X;
   mode å_Measure of S -> Function of S,R_EAL means
:: MEASURE1: def 11
it is nonnegative &
         it.í = 0.&
         for F being Sep_Sequence of S holds
         SUM(itùF) = it.(union rng F);
end;
*** change for:  sigma_Measure

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

5.

SPPOL_2.

definition
 mode S-Sequence_in_Rý is being_S-Seq FinSequence of TOP-REAL 2;
end;
*** change for:  S-Sequence_in_R2

definition
 mode Special_polygon_in_Rý is special_polygonal Subset of TOP-REAL 2;
end;
*** change for:  Special_polygon_in_R2

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Definitions of attributes:

1.

definition let IT be non empty GroupStr;
 attr IT is Group_with_the_operator_«-like means
:: MIDSP_2: def 5
  (for a being Element of the carrier of IT
      ex x being Element of the carrier of IT st 2ùx = a)
       &  for a being Element of the carrier of IT
         holds 2ùa = 0.IT implies a = 0.IT;
end;
*** change for:  midpoint_operator

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

2.

definition let IT be non empty QuantaleStr;
 attr IT is à-additive means
:: QUANTAL1: def 7
  for a,b,c being Element of the carrier of IT holds
     (aÀÙb)àc = (aàc)ÀÙ(bàc) & cà(aÀÙb) = (càa)ÀÙ(càb);
*** change for:  times-additive

 attr IT is à-continuous means
:: QUANTAL1: def 8
  for X1, X2 being Subset of IT st X1 is directed & X2 is directed holds
   (\/X1)à(\/X2) = \/({a à b where
      a is Element of the carrier of IT, b is Element of the carrier of IT:
     a î X1 & b î X2},IT);
end;
*** change for:  times-continuous

definition let Q be non empty QuantaleStr;
   let IT be UnOp of Q;
  attr IT is à-monotone means
:: QUANTAL1: def 14
   for a,b being Element of the carrier of Q holds IT.a à IT.b óó IT.(a à b);
end;
*** change for:  times-monotone

3.

definition
   let X be set;
   let IT be Dom_set_fam of X;
   attr IT is å_Field_Subset-like means
:: MEASURE1: def 9
(for A being set holds A î IT implies X\A î IT) &
     (for M being N_Sub_set_fam of X holds
     ((M c= IT) implies (union M î IT)));
end;
*** change for:  sigma_Field_Subset-like

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

4.

definition
 let S be ManySortedSign;
 attr S is ë-concrete means
:: CATALG_1: def 9

  ex f being Function of NAT,NAT st
   (for s being set st s î the carrier of S
     ex i being Nat, p being FinSequence st s = [i,p] & len p = f.i &
       [:{i}, (f.i)-tuples_on underlay S:] c= the carrier of S) &
   (for o being set st o î the OperSymbols of S
     ex i being Nat, p being FinSequence st o = [i,p] & len p = f.i &
       [:{i}, (f.i)-tuples_on underlay S:] c= the OperSymbols of S);
end;
*** change for:  delta-concrete

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

5.

reserve r,g for Real;
reserve seq for Real_Sequence;
reserve f for PartFunc of REAL,REAL;

definition let seq;
 attr seq is divergent_to_+ì means
:: LIMFUNC1: def 4
  for r ex n st for m st nóm holds r<seq.m;
*** change for:  divergent_to+infty

 attr seq is divergent_to_-ì means
:: LIMFUNC1: def 5
  for r ex n st for m st nóm holds seq.m<r;
end;
*** change for:  divergent_to-infty

definition let f;
attr f is convergent_in_+ì means
:: LIMFUNC1: def 6
 (for r ex g st r<g & gîdom f) &
 ex g st for seq st seq is divergent_to_+ì & rng seq c= dom f holds
  fùseq is convergent & lim(fùseq)=g;
*** change for:  convergent_in+infty

attr f is divergent_in_+ì_to_+ì means
:: LIMFUNC1: def 7
 (for r ex g st r<g & gîdom f) &
 for seq st seq is divergent_to_+ì & rng seq c= dom f holds
  fùseq is divergent_to_+ì;
*** change for:  divergent_in+infty_to+infty

attr f is divergent_in_+ì_to_-ì means
:: LIMFUNC1: def 8
 (for r ex g st r<g & gîdom f) &
 for seq st seq is divergent_to_+ì & rng seq c= dom f holds
  fùseq is divergent_to_-ì;
*** change for:  divergent_in-infty_to-infty

attr f is convergent_in_-ì means
:: LIMFUNC1: def 9
 (for r ex g st g<r & gîdom f) &
 ex g st for seq st seq is divergent_to_-ì & rng seq c= dom f holds
  fùseq is convergent & lim(fùseq)=g;
*** change for:  convergent_in-infty

attr f is divergent_in_-ì_to_+ì means
:: LIMFUNC1: def 10
 (for r ex g st g<r & gîdom f) &
 for seq st seq is divergent_to_-ì & rng seq c= dom f holds
  fùseq is divergent_to_+ì;
*** change for:  divergent_in-infty_to+infty

attr f is divergent_in_-ì_to_-ì means
:: LIMFUNC1: def 11
 (for r ex g st g<r & gîdom f) &
 for seq st seq is divergent_to_-ì & rng seq c= dom f holds
  fùseq is divergent_to_-ì;
end;
*** change for:  divergent_in-infty_to-infty

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

6.

 reserve X,x,y for set,

 definition let X;
  attr X is î-transitive means
:: ORDINAL1: def 2
 for x st x î X holds x c= X ;
*** change for:  epsilon-transitive

  attr X is î-connected means
:: ORDINAL1: def 3
 for x,y st x î X & y î X holds x î y or x = y or y î x ;
 end;
*** change for:  epsilon-connected

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

7.

definition let X be set;
 attr X is U-directed means
:: COHSP_1: def 4
  for Y being finite Subset of X ex a being set st union Y c= a & a î X;
***  change for:  c=directed

 attr X is ï-directed means
:: COHSP_1: def 5
  for Y being finite Subset of X
   ex a being set st (for y being set st y î Y holds a c= y) & a î X;
end;
*** change for c=filtered

definition let X be set;
 attr X is ï-closed means
:: COHSP_1: def 6
  for x,y being set st x î X & y î X holds x ï y î X;
end;
*** change for:  multiplicative

definition let f be Function;
 attr f is ï-distributive means
:: COHSP_1: def 13
  for a,b being set st dom f includes_lattice_of a, b holds
   f.(aïb) = f.a ï f.b;
end;
*** change for:  cap-distributive

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Definitions of functors:

1.

definition
   let X be set;
   let C be C_Measure of X;
func å_Field(C) -> Dom_set_fam of X means
:: MEASURE4: def 3
for A being Element of bool X holds
      (A î it iff for W,Z being Element of bool X holds
      (W c= A & Z c= X \ A implies C.W + C.Z <= C.(W U Z)));
end;

*** change for:  sigma_Field


definition
   let X be set;
   let C be C_Measure of X;
func å_Meas(C) -> Function of å_Field(C),R_EAL means
:: MEASURE4: def 4
for A being Element of bool X holds
     A î å_Field(C) implies it.A = C.A;
end;

*** change for:  sigma_Meas