[mizar] Last revision

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

Two more changes doen in the last revision (Mizar 7.8.04 MML 4.80.962):

A. The Swap functor originaly introduced in FINSEQ_7 was generalized and 
put in FUNCT_7;

  let F be Function; let x,y be set;
  func Swap(F,x,y) equals
:: FUNCT_7:def 12
    F+*(x,F.y)+*(y,F.x) if x in dom F & y in dom F
      otherwise F;

the original definition was left as a redefinition:

  let D be non empty set;
  let f be FinSequence of D;
  let i, j be Nat;
  redefine func Swap(f, i, j) -> FinSequence of D equals
:: FINSEQ_7:def 2
      Replace(Replace(f, i, f/.j), j, f/.i)
        if 1 <= i & i <= len f & 1 <= j & j <= len f
      otherwise f;


B. Because we cannot redefine or register numerals it is useful to
   have an identity functor for natural numbers.

    Such a functor was introduced twice: in ALGSEQ_1 (under the name 
PSeg, however the Mother Type was "Subset of NAT", not "Nat") and in 
GR_CY_1 (under the name Segm; actually it was a permissive definition, 
with the Mother Type: "non empty Subset of Nat" under the condition that 
the argument is non zero).

let n be natural number;
  func Segm n -> set equals
:: CARD_1:def 12
   n;

with a redefinition (to get "Subset of NAT') is now in CARD_1.

The definition in ALGSEQ_1 is removed, and in GR_CY_1 is substituted by 
a registration:

registration let n be non zero natural number;
 cluster Segm n -> non empty;
end;

The original definitions has the definiens
      { k : k < n }
so one have to refer to AXIOMS:30, sometimes.

Regards,
Andrzej