:: Regular Expression Quantifiers -- at least $m$ Occurrences
::  by Micha{\l} Trybulec
::
:: Received October 9, 2007
:: Copyright (c) 2007-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, SUBSET_1, AFINSQ_1, NAT_1, TARSKI, RELAT_1, PRE_POLY,
      XXREAL_0, NEWTON, SETFAM_1, XBOOLE_0, CARD_1, ARYTM_3, ORDINAL4, MODAL_1,
      FLANG_3;
 notations TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XCMPLX_0, ORDINAL1, SETFAM_1,
      XXREAL_0, AFINSQ_1, FLANG_1, FLANG_2;
 constructors NAT_1, XREAL_0, FLANG_1, FLANG_2;
 registrations SUBSET_1, NAT_1, ORDINAL1, AFINSQ_1, XREAL_0, XBOOLE_0,
      XXREAL_0;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
 definitions TARSKI;
 theorems NAT_1, TARSKI, XBOOLE_0, XBOOLE_1, XREAL_1, ZFMISC_1, FLANG_1,
      XXREAL_0, FLANG_2;
 schemes CARD_FIL, DOMAIN_1, NAT_1;

begin

reserve E, x, y, X for set;
reserve A, B, C for Subset of E^omega;
reserve a, a1, a2, b for Element of E^omega;

reserve i, k, l, m, n for Nat;

theorem
  B c= A* implies A* ^^ B c= A* & B ^^ (A*) c= A*
proof
  assume
A1: B c= A*;
  then
A2: B ^^ (A*) c= A* ^^ (A*) by FLANG_1:17;
  A* ^^ B c= A* ^^ (A*) by A1,FLANG_1:17;
  hence thesis by A2,FLANG_1:63;
end;

begin

:: At least n Occurences
:: Definition of |^.. n

definition
  let E, A, n;
  func A |^.. n -> Subset of E^omega equals
  union { B: ex m st n <= m & B = A
  |^ m };
  coherence
  proof
    defpred P[set] means ex m st n <= m & $1 = A |^ m;
    reconsider M = { B: P[B] } as Subset-Family of E^omega from DOMAIN_1:sch 7;
    union M is Subset of E^omega;
    hence thesis;
  end;
end;

:: At least n Occurences
:: Properties of |^.. n

theorem Th2:
  x in A |^.. n iff ex m st n <= m & x in A |^ m
proof
  thus x in A |^.. n implies ex m st n <= m & x in A |^ m
  proof
    defpred P[set] means ex m st n <= m & $1 = A |^ m;
    assume x in A |^.. n;
    then consider X such that
A1: x in X and
A2: X in { B: ex m st n <= m & B = A |^ m } by TARSKI:def 4;
A3: X in { B: P[B] } by A2;
    P[X] from CARD_FIL:sch 1(A3);
    hence thesis by A1;
  end;
  given m such that
A4: n <= m and
A5: x in A |^ m;
  defpred P[set] means ex m st n <= m & $1 = A |^ m;
  consider B such that
A6: x in B and
A7: P[B] by A4,A5;
  reconsider A = { C : P[C] } as Subset-Family of E^omega from DOMAIN_1:sch 7;
  B in A by A7;
  hence thesis by A6,TARSKI:def 4;
end;

theorem Th3:
  n <= m implies A |^ m c= A |^.. n
proof
  assume n <= m;
  then for x holds x in A |^ m implies x in A |^.. n by Th2;
  hence thesis by TARSKI:def 3;
end;

theorem Th4:
  A |^.. n = {} iff n > 0 & A = {}
proof
  thus A |^.. n = {} implies n > 0 & A = {}
  proof
A1: A <> {} implies A |^.. n <> {}
    proof
      assume
A2:   A <> {};
      now
        let m;
        consider m such that
A3:     n <= m;
        A |^ m <> {} by A2,FLANG_1:27;
        then ex x st x in A |^ m by XBOOLE_0:def 1;
        hence thesis by A3,Th2;
      end;
      hence thesis;
    end;
    assume that
A4: A |^.. n = {} and
A5: n <= 0 or A <> {};
    n <= 0 implies <%>E in A |^.. n
    proof
      assume n <= 0;
      then
A6:   n = 0;
      A |^ 0 c= A |^.. 0 by Th3;
      then {<%>E} c= A |^.. 0 by FLANG_1:24;
      hence thesis by A6,ZFMISC_1:31;
    end;
    hence contradiction by A4,A5,A1;
  end;
  assume that
A7: n > 0 and
A8: A = {};
  now
    let x;
    assume x in A |^.. n;
    then ex m st n <= m & x in A |^ m by Th2;
    hence contradiction by A7,A8,FLANG_1:27;
  end;
  hence thesis by XBOOLE_0:def 1;
end;

theorem Th5:
  m <= n implies A |^.. n c= A |^.. m
proof
  assume
A1: m <= n;
  now
    let x;
    assume x in A |^.. n;
    then consider k such that
A2: n <= k and
A3: x in A |^ k by Th2;
    m <= k by A1,A2,XXREAL_0:2;
    hence x in A |^.. m by A3,Th2;
  end;
  hence thesis by TARSKI:def 3;
end;

theorem Th6:
  k <= m implies A |^ (m, n) c= A |^.. k
proof
  assume
A1: k <= m;
  now
    let x;
    assume x in A |^ (m, n);
    then consider l such that
A2: m <= l and
    l <= n and
A3: x in A |^ l by FLANG_2:19;
    k <= l by A1,A2,XXREAL_0:2;
    hence x in A |^.. k by A3,Th2;
  end;
  hence thesis by TARSKI:def 3;
end;

theorem Th7:
  m <= n + 1 implies A |^ (m, n) \/ A |^.. (n + 1) = A |^.. m
proof
  assume m <= n + 1;
  then
A1: A |^.. (n + 1) c= A |^.. m by Th5;
  now
    let x;
    assume x in A |^.. m;
    then consider k such that
A2: m <= k and
A3: x in A |^ k by Th2;
A4: now
      assume k > n;
      then k >= n + 1 by NAT_1:13;
      hence x in A |^.. (n + 1) by A3,Th2;
    end;
    k <= n implies x in A |^ (m, n) by A2,A3,FLANG_2:19;
    hence x in A |^ (m, n) \/ A |^.. (n + 1) by A4,XBOOLE_0:def 3;
  end;
  then
A5: A |^.. m c= A |^ (m, n) \/ A |^.. (n + 1) by TARSKI:def 3;
  A |^ (m, n) c= A |^.. m by Th6;
  then A |^ (m, n) \/ A |^.. (n + 1) c= A |^.. m by A1,XBOOLE_1:8;
  hence thesis by A5,XBOOLE_0:def 10;
end;

theorem
  A |^ n \/ A |^.. (n + 1) = A |^.. n
proof
A1: n <= n + 1 by NAT_1:13;
  thus A |^ n \/ A |^.. (n + 1) = A |^ (n, n) \/ A |^.. (n + 1) by FLANG_2:22
    .= A |^.. n by A1,Th7;
end;

theorem Th9:
  A |^.. n c= A*
proof
  now
    let x;
    assume x in A |^.. n;
    then ex k st n <= k & x in A |^ k by Th2;
    hence x in A* by FLANG_1:41;
  end;
  hence thesis by TARSKI:def 3;
end;

theorem Th10:
  <%>E in A |^.. n iff n = 0 or <%>E in A
proof
  thus <%>E in A |^.. n implies n = 0 or <%>E in A
  proof
    assume <%>E in A |^.. n;
    then
A1: ex k st n <= k & <%>E in A |^ k by Th2;
    n = 0 or n > 0;
    hence thesis by A1,FLANG_1:31;
  end;
  assume
A2: n = 0 or <%>E in A;
  per cases by A2;
  suppose
A3: n = 0;
    {<%>E} = A |^ 0 by FLANG_1:24;
    then <%>E in A |^ n by A3,TARSKI:def 1;
    hence thesis by Th2;
  end;
  suppose
    <%>E in A;
    then <%>E in A |^ n by FLANG_1:30;
    hence thesis by Th2;
  end;
end;

theorem Th11:
  A |^.. n = A* iff <%>E in A or n = 0
proof
  thus A |^.. n = A* implies <%>E in A or n = 0
  proof
    assume that
A1: A |^.. n = A* and
A2: not <%>E in A and
A3: n <> 0;
    <%>E in A* by FLANG_1:48;
    hence contradiction by A1,A2,A3,Th10;
  end;
  assume
A4: <%>E in A or n = 0;
    now
      let x;
      assume x in A*;
      then consider k such that
A5:   x in A |^ k by FLANG_1:41;
      per cases;
      suppose
        n <= k;
        hence x in A |^.. n by A5,Th2;
      end;
      suppose
        k < n;
        then A |^ k c= A |^ n by A4,FLANG_1:36;
        hence x in A |^.. n by A5,Th2;
      end;
    end;
    then
A6: A* c= A |^.. n by TARSKI:def 3;
    A |^.. n c= A* by Th9;
    hence thesis by A6,XBOOLE_0:def 10;
end;

theorem
  A* = A |^ (0, n) \/ A |^.. (n + 1)
proof
  thus A* = A |^.. 0 by Th11
    .= A |^ (0, n) \/ A |^.. (n + 1) by Th7;
end;

theorem Th13:
  A c= B implies A |^.. n c= B |^.. n
proof
  assume
A1: A c= B;
  now
    let x;
    assume x in A |^.. n;
    then consider k such that
A2: n <= k and
A3: x in A |^ k by Th2;
    A |^ k c= B |^ k by A1,FLANG_1:37;
    hence x in B |^.. n by A2,A3,Th2;
  end;
  hence thesis by TARSKI:def 3;
end;

theorem Th14:
  x in A & x <> <%>E implies A |^.. n <> {<%>E}
proof
  assume that
A1: x in A and
A2: x <> <%>E;
  per cases;
  suppose
A3: n = 0;
    x in A |^ 1 by A1,FLANG_1:25;
    then x in A |^.. n by A3,Th2;
    hence thesis by A2,TARSKI:def 1;
  end;
  suppose
A4: n > 0;
A5: A |^ n <> {} by A1,FLANG_1:27;
    A |^ n <> {<%>E} by A1,A2,A4,FLANG_2:7;
    then consider y such that
A6: y in A |^ n and
A7: y <> <%>E by A5,ZFMISC_1:35;
    y in A |^.. n by A6,Th2;
    hence thesis by A7,TARSKI:def 1;
  end;
end;

theorem Th15:
  A |^.. n = {<%>E} iff A = {<%>E} or n = 0 & A = {}
proof
  thus A |^.. n = {<%>E} implies A = {<%>E} or n = 0 & A = {}
  proof
    assume that
A1: A |^.. n = {<%>E} and
A2: A <> {<%>E} and
A3: n <> 0 or A <> {};
    per cases by A3;
    suppose
A4:   n <> 0;
      <%>E in A |^.. n by A1,ZFMISC_1:31;
      then consider k such that
A5:   n <= k and
A6:   <%>E in A |^ k by Th2;
      k > 0 by A4,A5;
      then
A7:   <%>E in A by A6,FLANG_1:31;
      not ex x st x in A & x <> <%>E by A1,Th14;
      hence contradiction by A2,A7,ZFMISC_1:35;
    end;
    suppose
      A <> {};
      then ex x st x in A & x <> <%>E by A2,ZFMISC_1:35;
      hence contradiction by A1,Th14;
    end;
  end;
  assume
A8: A = {<%>E} or n = 0 & A = {};
  per cases by A8;
  suppose
A9: A = {<%>E};
A10: now
      let x;
      assume x in {<%>E};
      then x in A |^ n by A9,FLANG_1:28;
      hence x in A |^.. n by Th2;
    end;
    now
      let x;
      assume x in A |^.. n;
      then ex k st n <= k & x in A |^ k by Th2;
      hence x in {<%>E} by A9,FLANG_1:28;
    end;
    hence thesis by A10,TARSKI:1;
  end;
  suppose
A11: n = 0 & A = {};
    hence A |^.. n = A* by Th11
      .= {<%>E} by A11,FLANG_1:47;
  end;
end;

theorem Th16:
  A |^.. (n + 1) = (A |^.. n) ^^ A
proof
  now
    let x;
    assume x in A |^.. (n + 1);
    then consider k such that
A1: n + 1 <= k and
A2: x in A |^ k by Th2;
    consider l such that
A3: l + 1 = k by A1,NAT_1:6;
    x in (A |^ l) ^^ (A |^ 1) by A2,A3,FLANG_1:33;
    then consider a, b such that
A4: a in A |^ l and
A5: b in A |^ 1 and
A6: x = a ^ b by FLANG_1:def 1;
    n <= l by A1,A3,XREAL_1:6;
    then a in A |^.. n by A4,Th2;
    then x in (A |^.. n) ^^ (A |^ 1) by A5,A6,FLANG_1:def 1;
    hence x in (A |^.. n) ^^ A by FLANG_1:25;
  end;
  then
A7: A |^.. (n + 1) c= (A |^.. n) ^^ A by TARSKI:def 3;
  now
    let x;
    assume x in (A |^.. n) ^^ A;
    then consider a, b such that
A8: a in (A |^.. n) and
A9: b in A and
A10: x = a ^ b by FLANG_1:def 1;
    consider k such that
A11: n <= k and
A12: a in A |^ k by A8,Th2;
A13: n + 1 <= k + 1 by A11,XREAL_1:6;
    b in A |^ 1 by A9,FLANG_1:25;
    then x in A |^ (k + 1) by A10,A12,FLANG_1:40;
    hence x in A |^.. (n + 1) by A13,Th2;
  end;
  then (A |^.. n) ^^ A c= A |^.. (n + 1) by TARSKI:def 3;
  hence thesis by A7,XBOOLE_0:def 10;
end;

theorem Th17:
  (A |^.. m) ^^ (A*) = A |^.. m
proof
  now
    let x;
    assume x in (A |^.. m) ^^ (A*);
    then consider a, b such that
A1: a in A |^.. m and
A2: b in A* and
A3: x = a ^ b by FLANG_1:def 1;
    consider k such that
A4: b in A |^ k by A2,FLANG_1:41;
    consider l such that
A5: m <= l and
A6: a in A |^ l by A1,Th2;
A7: l + k >= m by A5,NAT_1:12;
    a ^ b in A |^ (l + k) by A4,A6,FLANG_1:40;
    hence x in A |^.. m by A3,A7,Th2;
  end;
  then
A8: (A |^.. m) ^^ (A*) c= A |^.. m by TARSKI:def 3;
  <%>E in A* by FLANG_1:48;
  then A |^.. m c= (A |^.. m) ^^ (A*) by FLANG_1:16;
  hence thesis by A8,XBOOLE_0:def 10;
end;

theorem Th18:
  (A |^.. m) ^^ (A |^.. n) = A |^.. (m + n)
proof
  defpred P[Nat] means (A |^.. m) ^^ (A |^.. $1) = A |^.. (m + $1);
A1: now
    let n;
    assume
A2: P[n];
    (A |^.. m) ^^ (A |^.. (n + 1)) = (A |^.. m) ^^ ((A |^.. n) ^^ A) by Th16
      .= A |^.. (m + n) ^^ A by A2,FLANG_1:18
      .= A |^.. (m + n + 1) by Th16;
    hence P[n + 1];
  end;
  (A |^.. m) ^^ (A |^.. 0) = (A |^.. m) ^^ (A*) by Th11
    .= (A |^.. (m + 0)) by Th17;
  then
A3: P[0];
  for n holds P[n] from NAT_1:sch 2(A3, A1);
  hence thesis;
end;

theorem Th19:
  n > 0 implies (A |^.. m) |^ n = A |^.. (m * n)
proof
  defpred P[Nat] means $1 > 0 implies (A |^.. m) |^ $1 = A |^.. (m * $1);
A1: now
    let n;
    assume
A2: P[n];
    now
      assume n + 1 > 0;
      per cases;
      suppose
        n = 0;
        hence (A |^.. m) |^ (n + 1) = A |^.. (m * (n + 1)) by FLANG_1:25;
      end;
      suppose
        n > 0;
        hence (A |^.. m) |^ (n + 1) = (A |^.. (m * n)) ^^ (A |^.. m) by A2,
FLANG_1:23
          .= A |^.. (m * n + m) by Th18
          .= A |^.. (m * (n + 1));
      end;
    end;
    hence P[n + 1];
  end;
A3: P[0];
  for n holds P[n] from NAT_1:sch 2(A3, A1);
  hence thesis;
end;

theorem
  (A |^.. n)* = (A |^.. n)?
proof
  now
    let x;
    assume x in (A |^.. n)*;
    then consider k such that
A1: x in (A |^.. n) |^ k by FLANG_1:41;
    per cases;
    suppose
      k = 0;
      then x in (A |^.. n) |^ 0 \/ (A |^.. n) |^ 1 by A1,XBOOLE_0:def 3;
      hence x in (A |^.. n)? by FLANG_2:75;
    end;
    suppose
A2:   k > 0;
      then (A |^.. n) |^ k c= A |^.. (n * k) by Th19;
      then consider l such that
A3:   n * k <= l and
A4:   x in A |^ l by A1,Th2;
      k >= 0 + 1 by A2,NAT_1:13;
      then n * k >= n by XREAL_1:151;
      then l >= n by A3,XXREAL_0:2;
      then x in A |^.. n by A4,Th2;
      then x in (A |^.. n) |^ 1 by FLANG_1:25;
      then x in (A |^.. n) |^ 0 \/ (A |^.. n) |^ 1 by XBOOLE_0:def 3;
      hence x in (A |^.. n)? by FLANG_2:75;
    end;
  end;
  then
A5: (A |^.. n)* c= (A |^.. n)? by TARSKI:def 3;
  (A |^.. n)? c= (A |^.. n)* by FLANG_2:86;
  hence thesis by A5,XBOOLE_0:def 10;
end;

theorem Th21:
  A c= C |^.. m & B c= C |^.. n implies A ^^ B c= C |^.. (m + n)
proof
  assume that
A1: A c= C |^.. m and
A2: B c= C |^.. n;
  thus x in A ^^ B implies x in C |^.. (m + n)
  proof
    assume x in A ^^ B;
    then consider a, b such that
A3: a in A and
A4: b in B and
A5: x = a ^ b by FLANG_1:def 1;
    a ^ b in (C |^.. m) ^^ (C |^.. n) by A1,A2,A3,A4,FLANG_1:def 1;
    hence thesis by A5,Th18;
  end;
end;

theorem Th22:
  A |^.. (n + k) = (A |^.. n) ^^ (A |^ k)
proof
  defpred P[Nat] means A |^.. (n + $1) = (A |^.. n) ^^ (A |^ $1);
A1: now
    let k be Nat;
    assume
A2: P[k];
    A |^.. (n + (k + 1)) = (A |^.. (n + k + 1))
      .= (A |^.. n) ^^ (A |^ k) ^^ A by A2,Th16
      .= (A |^.. n) ^^ ((A |^ k) ^^ A) by FLANG_1:18
      .= (A |^.. n) ^^ (A |^ (k + 1)) by FLANG_1:23;
    hence P[k + 1];
  end;
  A |^.. (n + 0) = (A |^.. n) ^^ {<%>E} by FLANG_1:13
    .= (A |^.. n) ^^ (A |^ 0) by FLANG_1:24;
  then
A3: P[0];
  for k being Nat holds P[k] from NAT_1:sch 2(A3, A1);
  hence thesis;
end;

theorem Th23:
  A ^^ (A |^.. n) = (A |^.. n) ^^ A
proof
  defpred P[Nat] means A ^^ (A |^.. $1) = (A |^.. $1) ^^ A;
A1: now
    let k be Nat;
    assume
A2: P[k];
    A ^^ (A |^.. (k + 1)) = A ^^ ((A |^.. k) ^^ A) by Th16
      .= (A |^.. k) ^^ A ^^ A by A2,FLANG_1:18
      .= (A |^.. (k + 1)) ^^ A by Th16;
    hence P[k + 1];
  end;
  A ^^ (A |^.. 0) = A ^^ (A*) by Th11
    .= (A*) ^^ A by FLANG_1:57
    .= (A |^.. 0) ^^ A by Th11;
  then
A3: P[0];
  for k being Nat holds P[k] from NAT_1:sch 2(A3, A1);
  hence thesis;
end;

theorem Th24:
  (A |^ k) ^^ (A |^.. n) = (A |^.. n) ^^ (A |^ k)
proof
  defpred P[Nat] means (A |^ $1) ^^ (A |^.. n) = (A |^.. n) ^^ (A |^ $1);
A1: now
    let k;
    assume
A2: P[k];
    (A |^ (k + 1)) ^^ (A |^.. n) = ((A |^ k) ^^ A) ^^ (A |^.. n) by FLANG_1:23
      .= (A ^^ (A |^ k)) ^^ (A |^.. n) by FLANG_1:32
      .= A ^^ ((A |^.. n) ^^ (A |^ k)) by A2,FLANG_1:18
      .= (A ^^ (A |^.. n)) ^^ (A |^ k) by FLANG_1:18
      .= (A |^.. n) ^^ A ^^ (A |^ k) by Th23
      .= (A |^.. n) ^^ (A ^^ (A |^ k)) by FLANG_1:18
      .= (A |^.. n) ^^ ((A |^ k) ^^ A) by FLANG_1:32
      .= (A |^.. n) ^^ (A |^ (k + 1)) by FLANG_1:23;
    hence P[k + 1];
  end;
  (A |^ 0) ^^ (A |^.. n) = {<%>E} ^^ (A |^.. n) by FLANG_1:24
    .= (A |^.. n) by FLANG_1:13
    .= (A |^.. n) ^^ {<%>E} by FLANG_1:13
    .= (A |^.. n) ^^ (A |^ 0) by FLANG_1:24;
  then
A3: P[0];
  for k holds P[k] from NAT_1:sch 2(A3, A1);
  hence thesis;
end;

theorem Th25:
  (A |^ (k, l)) ^^ (A |^.. n) = (A |^.. n) ^^ (A |^ (k, l))
proof
  defpred P[Nat] means (A |^ (k, l)) ^^ (A |^.. $1) = (A |^.. $1) ^^ (A |^ (k,
  l));
A1: now
    let n;
    assume
A2: P[n];
    (A |^ (k, l)) ^^ (A |^.. (n + 1)) = (A |^ (k, l)) ^^ ((A |^.. n) ^^ A)
    by Th16
      .= (A |^.. n) ^^ (A |^ (k, l)) ^^ A by A2,FLANG_1:18
      .= (A |^.. n) ^^ ((A |^ (k, l)) ^^ A) by FLANG_1:18
      .= (A |^.. n) ^^ (A ^^ (A |^ (k, l))) by FLANG_2:36
      .= (A |^.. n) ^^ A ^^ (A |^ (k, l)) by FLANG_1:18
      .= (A |^.. (n + 1)) ^^ (A |^ (k, l)) by Th16;
    hence P[n + 1];
  end;
  (A |^ (k, l)) ^^ (A |^.. 0) = (A |^ (k, l)) ^^ (A*) by Th11
    .= A* ^^ (A |^ (k, l)) by FLANG_2:66
    .= (A |^.. 0) ^^ (A |^ (k, l)) by Th11;
  then
A3: P[0];
  for n holds P[n] from NAT_1:sch 2(A3, A1);
  hence thesis;
end;

theorem
  <%>E in B implies A c= A ^^ (B |^.. n) & A c= (B |^.. n) ^^ A
proof
  assume <%>E in B;
  then <%>E in B |^.. n by Th10;
  hence thesis by FLANG_1:16;
end;

theorem Th27:
  (A |^.. m) ^^ (A |^.. n) = (A |^.. n) ^^ (A |^.. m)
proof
  thus (A |^.. m) ^^ (A |^.. n) = A |^.. (m + n) by Th18
    .= (A |^.. n) ^^ (A |^.. m) by Th18;
end;

theorem Th28:
  A c= B |^.. k & n > 0 implies A |^ n c= B |^.. k
proof
  assume that
A1: A c= B |^.. k and
A2: n > 0;
  defpred P[Nat] means $1 > 0 implies A |^ $1 c= B |^.. k;
A3: now
    let m;
    assume
A4: P[m];
    per cases;
    suppose
      m <= 0;
      then m = 0;
      hence P[m + 1] by A1,FLANG_1:25;
    end;
    suppose
      m > 0;
      then (A |^ m) ^^ A c= (B |^.. k) ^^ (B |^.. k) by A1,A4,FLANG_1:17;
      then A |^ (m + 1) c= (B |^.. k) ^^ (B |^.. k) by FLANG_1:23;
      then
A5:   A |^ (m + 1) c= (B |^.. (k + k)) by Th18;
      B |^.. (k + k) c= B |^.. k by Th5,NAT_1:11;
      hence P[m + 1] by A5,XBOOLE_1:1;
    end;
  end;
A6: P[0];
  for m holds P[m] from NAT_1:sch 2(A6, A3);
  hence thesis by A2;
end;

theorem Th29:
  A c= B |^.. k & n > 0 implies A |^.. n c= B |^.. k
proof
  assume that
A1: A c= B |^.. k and
A2: n > 0;
  let x;
  assume x in A |^.. n;
  then consider m such that
A3: m >= n and
A4: x in A |^ m by Th2;
  A |^ m c= B |^.. k by A1,A2,A3,Th28;
  hence thesis by A4;
end;

theorem Th30:
  A* ^^ A = A |^.. 1
proof
A1: now
    let x;
    assume x in (A*) ^^ A;
    then consider a1, a2 such that
A2: a1 in A* and
A3: a2 in A and
A4: x = a1 ^ a2 by FLANG_1:def 1;
    consider n such that
A5: a1 in A |^ n by A2,FLANG_1:41;
A6: n + 1 >= 1 by NAT_1:11;
    a2 in A |^ 1 by A3,FLANG_1:25;
    then a1 ^ a2 in A |^ (n + 1) by A5,FLANG_1:40;
    hence x in A |^.. 1 by A4,A6,Th2;
  end;
  now
    let x;
    assume x in A |^.. 1;
    then consider n such that
A7: n >= 1 and
A8: x in A |^ n by Th2;
    consider m such that
A9: m + 1 = n by A7,NAT_1:6;
    A |^ (m + 1) c= (A*) ^^ A by FLANG_1:51;
    hence x in (A*) ^^ A by A8,A9;
  end;
  hence thesis by A1,TARSKI:1;
end;

theorem
  A* ^^ (A |^ k) = A |^.. k
proof
  defpred P[Nat] means A* ^^ (A |^ $1) = A |^.. $1;
A1: now
    let k;
    assume
A2: P[k];
    A* ^^ (A |^ (k + 1)) = A* ^^ ((A |^ k) ^^ A) by FLANG_1:23
      .= A |^.. k ^^ A by A2,FLANG_1:18
      .= A |^.. (k + 1) by Th16;
    hence P[k + 1];
  end;
  A* ^^ (A |^ 0) = A* ^^ {<%>E} by FLANG_1:24
    .= A* by FLANG_1:13
    .= A |^.. 0 by Th11;
  then
A3: P[0];
  for k holds P[k] from NAT_1:sch 2(A3, A1);
  hence thesis;
end;

theorem Th32:
  (A |^.. m) ^^ (A*) = A* ^^ (A |^.. m)
proof
  thus (A |^.. m) ^^ (A*) = (A |^.. m) ^^ (A |^.. 0) by Th11
    .= (A |^.. 0) ^^ (A |^.. m) by Th27
    .= A* ^^ (A |^.. m) by Th11;
end;

theorem Th33:
  k <= l implies (A |^.. n) ^^ (A |^ (k, l)) = A |^.. (n + k)
proof
  assume
A1: k <= l;
A2: A |^.. (n + k) c= (A |^.. n) ^^ (A |^ (k, l))
  proof
    let x;
    assume x in A |^.. (n + k);
    then consider i such that
A3: i >= n + k and
A4: x in A |^ i by Th2;
    consider m such that
A5: n + k + m = i by A3,NAT_1:10;
    i = n + m + k by A5;
    then x in (A |^ (n + m)) ^^ (A |^ k) by A4,FLANG_1:33;
    then
A6: ex a, b st a in A |^ (n + m) & b in A |^ k & x = a ^ b by FLANG_1:def 1;
A7: A |^ (n + m) c= A |^.. n by Th3,NAT_1:11;
    A |^ k c= A |^ (k, l) by A1,FLANG_2:20;
    hence thesis by A6,A7,FLANG_1:def 1;
  end;
  (A |^.. n) ^^ (A |^ (k, l)) c= A |^.. (n + k)
  proof
    let x;
    assume x in (A |^.. n) ^^ (A |^ (k, l));
    then consider a, b such that
A8: a in A |^.. n and
A9: b in A |^ (k, l) and
A10: x = a ^ b by FLANG_1:def 1;
    A |^ (k, l) c= A |^.. k by Th6;
    then a ^ b in (A |^.. n) ^^ (A |^.. k) by A8,A9,FLANG_1:def 1;
    hence thesis by A10,Th18;
  end;
  hence thesis by A2,XBOOLE_0:def 10;
end;

theorem
  k <= l implies A* ^^ (A |^ (k, l)) = A |^.. k
proof
  assume k <= l;
  then (A |^.. 0) ^^ (A |^ (k, l)) = A |^.. (0 + k) by Th33;
  hence thesis by Th11;
end;

theorem Th35:
  (A |^ m) |^.. n c= A |^.. (m * n)
proof
  let x;
  assume x in (A |^ m) |^.. n;
  then consider k such that
A1: k >= n and
A2: x in (A |^ m) |^ k by Th2;
A3: m * k >= m * n by A1,XREAL_1:64;
  x in A |^ (m * k) by A2,FLANG_1:34;
  hence thesis by A3,Th2;
end;

theorem
  (A |^ m) |^.. n c= (A |^.. n) |^ m
proof
  per cases;
  suppose
A1: m > 0;
    (A |^ m) |^.. n c= A |^.. (m * n) by Th35;
    hence thesis by A1,Th19;
  end;
  suppose
    m <= 0;
    then
A2: m = 0;
    then (A |^ m) |^.. n = {<%>E} |^.. n by FLANG_1:24
      .= {<%>E} by Th15
      .= (A |^.. n) |^ m by A2,FLANG_1:24;
    hence thesis;
  end;
end;

theorem Th37:
  a in C |^.. m & b in C |^.. n implies a ^ b in C |^.. (m + n)
proof
  assume that
A1: a in C |^.. m and
A2: b in C |^.. n;
A3: (C |^.. m) ^^ (C |^.. n) c= C |^.. (m + n) by Th21;
  a ^ b in (C |^.. m) ^^ (C |^.. n) by A1,A2,FLANG_1:def 1;
  hence thesis by A3;
end;

theorem Th38:
  A |^.. k = {x} implies x = <%>E
proof
  assume that
A1: A |^.. k = {x} and
A2: x <> <%>E;
  reconsider a = x as Element of E^omega by A1,ZFMISC_1:31;
  x in A |^.. k by A1,ZFMISC_1:31;
  then
A3: a ^ a in A |^.. (k + k) by Th37;
A4: A |^.. (k + k) c= A |^.. k by Th5,NAT_1:11;
  a ^ a <> x by A2,FLANG_1:11;
  hence thesis by A1,A4,A3,TARSKI:def 1;
end;

theorem
  A c= B* implies A |^.. n c= B*
proof
  assume
A1: A c= B*;
  let x;
  assume x in A |^.. n;
  then consider k such that
  k >= n and
A2: x in A |^ k by Th2;
  A |^ k c= B* by A1,FLANG_1:59;
  hence thesis by A2;
end;

theorem Th40:
  A? c= A |^.. k iff k = 0 or <%>E in A
proof
  thus A? c= A |^.. k implies k = 0 or <%>E in A
  proof
A1: <%>E in A? by FLANG_2:78;
    assume A? c= A |^.. k;
    hence thesis by A1,Th10;
  end;
  assume k = 0 or <%>E in A;
  then A |^.. k = A* by Th11;
  hence thesis by FLANG_2:86;
end;

theorem Th41:
  A |^.. k ^^ (A?) = A |^.. k
proof
  thus A |^.. k ^^ (A?) = A |^.. k ^^ (A |^ (0, 1)) by FLANG_2:79
    .= A |^.. (k + 0) by Th33
    .= A |^.. k;
end;

theorem
  A |^.. k ^^ (A?) = A? ^^ (A |^.. k)
proof
  thus A |^.. k ^^ (A?) = A |^.. k ^^ (A |^ (0, 1)) by FLANG_2:79
    .= A |^ (0, 1) ^^ (A |^.. k) by Th25
    .= A? ^^ (A |^.. k) by FLANG_2:79;
end;

theorem
  B c= A* implies A |^.. k ^^ B c= A |^.. k & B ^^ (A |^.. k) c= A |^.. k
proof
  assume
A1: B c= A*;
  then B ^^ (A |^.. k) c= A* ^^ (A |^.. k) by FLANG_1:17;
  then
A2: B ^^ (A |^.. k) c= A |^.. k ^^ (A*) by Th32;
  A |^.. k ^^ B c= A |^.. k ^^ (A*) by A1,FLANG_1:17;
  hence thesis by A2,Th17;
end;

theorem Th44:
  (A /\ B) |^.. k c= (A |^.. k) /\ (B |^.. k)
proof
  thus x in (A /\ B) |^.. k implies x in (A |^.. k) /\ (B |^.. k)
  proof
    assume x in (A /\ B) |^.. k;
    then consider m such that
A1: k <= m and
A2: x in (A /\ B) |^ m by Th2;
A3: B |^ m c= B |^.. k by A1,Th3;
    (A /\ B) |^ m c= (A |^ m) /\ (B |^ m) by FLANG_1:39;
    then
A4: x in (A |^ m) /\ (B |^ m) by A2;
    A |^ m c= A |^.. k by A1,Th3;
    then (A |^ m) /\ (B |^ m) c= (A |^.. k) /\ (B |^.. k) by A3,XBOOLE_1:27;
    hence thesis by A4;
  end;
end;

theorem Th45:
  (A |^.. k) \/ (B |^.. k) c= (A \/ B) |^.. k
proof
  thus x in (A |^.. k) \/ (B |^.. k) implies x in (A \/ B) |^.. k
  proof
    assume
A1: x in (A |^.. k) \/ (B |^.. k);
    per cases by A1,XBOOLE_0:def 3;
    suppose
      x in (A |^.. k);
      then consider m such that
A2:   k <= m and
A3:   x in A |^ m by Th2;
A4:   (A |^ m) \/ (B |^ m) c= (A \/ B) |^ m by FLANG_1:38;
      A |^ m c= (A |^ m) \/ (B |^ m) by XBOOLE_1:7;
      then A |^ m c= (A \/ B) |^ m by A4,XBOOLE_1:1;
      then
A5:   x in (A \/ B) |^ m by A3;
      (A \/ B) |^ m c= (A \/ B) |^.. k by A2,Th3;
      hence thesis by A5;
    end;
    suppose
      x in (B |^.. k);
      then consider m such that
A6:   k <= m and
A7:   x in B |^ m by Th2;
A8:   (A |^ m) \/ (B |^ m) c= (A \/ B) |^ m by FLANG_1:38;
      B |^ m c= (A |^ m) \/ (B |^ m) by XBOOLE_1:7;
      then B |^ m c= (A \/ B) |^ m by A8,XBOOLE_1:1;
      then
A9:   x in (A \/ B) |^ m by A7;
      (A \/ B) |^ m c= (A \/ B) |^.. k by A6,Th3;
      hence thesis by A9;
    end;
  end;
end;

theorem Th46:
  <%x%> in A |^.. k iff <%x%> in A & (<%>E in A or k <= 1)
proof
  thus <%x%> in A |^.. k implies <%x%> in A & (<%>E in A or k <= 1)
  proof
    assume <%x%> in A |^.. k;
    then ex m st k <= m & <%x%> in A |^ m by Th2;
    hence thesis by FLANG_2:9;
  end;
  assume that
A1: <%x%> in A and
A2: <%>E in A or k <= 1;
  per cases by A2,NAT_1:25;
  suppose
    <%>E in A & k > 1;
    then <%x%> in A |^ k by A1,FLANG_2:9;
    hence thesis by Th2;
  end;
  suppose
    k = 0;
    then A |^.. k = A* by Th11;
    hence thesis by A1,FLANG_1:72;
  end;
  suppose
    k = 1;
    then <%x%> in A |^ k by A1,FLANG_1:25;
    hence thesis by Th2;
  end;
end;

theorem Th47:
  A c= B |^.. k implies B |^.. k = (B \/ A) |^.. k
proof
  defpred P[Nat] means $1 >= k implies (B \/ A) |^ $1 c= B |^.. k;
  B |^ 1 c= B |^.. 1 by Th3;
  then
A1: B c= B |^.. 1 by FLANG_1:25;
  assume
A2: A c= B |^.. k;
A3: now
    let n;
    assume
A4: P[n];
    now
      assume
A5:   n + 1 >= k;
      per cases by A5,NAT_1:8;
      suppose
A6:     n + 1 = k;
        per cases;
        suppose
          k = 0;
          hence (B \/ A) |^ (n + 1) c= B |^.. k by A6;
        end;
        suppose
A7:       k > 0;
          then k >= 0 + 1 by NAT_1:13;
          then B |^.. k c= B |^.. 1 by Th5;
          then A c= B |^.. 1 by A2,XBOOLE_1:1;
          then B \/ A c= B |^.. 1 by A1,XBOOLE_1:8;
          then
A8:       (B \/ A) |^ k c= (B |^.. 1) |^ k by FLANG_1:37;
          (B |^.. 1) |^ k c= B |^.. (1 * k) by A7,Th19;
          hence (B \/ A) |^ (n + 1) c= B |^.. k by A6,A8,XBOOLE_1:1;
        end;
      end;
      suppose
A9:     n >= k;
A10:    B |^.. (k + k) c= B |^.. k by Th5,NAT_1:11;
        (B \/ A) |^ n ^^ A c= B |^.. (k + k) by A2,A4,A9,Th21;
        then
A11:    (B \/ A) |^ n ^^ A c= B |^.. k by A10,XBOOLE_1:1;
A12:    B |^.. (k + 1) c= B |^.. k by Th5,NAT_1:11;
        (B \/ A) |^ n ^^ B c= B |^.. (k + 1) by A1,A4,A9,Th21;
        then
A13:    (B \/ A) |^ n ^^ B c= B |^.. k by A12,XBOOLE_1:1;
        (B \/ A) |^ (n + 1) = (B \/ A) |^ n ^^ (B \/ A) by FLANG_1:23
          .= (B \/ A) |^ n ^^ B \/ (B \/ A) |^ n ^^ A by FLANG_1:20;
        hence (B \/ A) |^ (n + 1) c= B |^.. k by A13,A11,XBOOLE_1:8;
      end;
    end;
    hence P[n + 1];
  end;
A14: P[0]
  proof
    assume 0 >= k;
    then k = 0;
    then
A15: B |^.. k = B* by Th11;
A16: <%>E in B* by FLANG_1:48;
    (B \/ A) |^ 0 = {<%>E} by FLANG_1:24;
    hence thesis by A15,A16,ZFMISC_1:31;
  end;
A17: for n holds P[n] from NAT_1:sch 2(A14, A3);
A18: (B \/ A) |^.. k c= B |^.. k
  proof
    let x;
    assume x in (B \/ A) |^.. k;
    then consider n such that
A19: n >= k and
A20: x in (B \/ A) |^ n by Th2;
    (B \/ A) |^ n c= B |^.. k by A17,A19;
    hence thesis by A20;
  end;
  B |^.. k c= (B \/ A) |^.. k by Th13,XBOOLE_1:7;
  hence thesis by A18,XBOOLE_0:def 10;
end;

begin

:: Positive Closure
:: Definition of +

definition
  let E, A;
  func A+ -> Subset of E^omega equals
  union { B: ex n st n > 0 & B = A |^ n };
  coherence
  proof
    defpred P[set] means ex n st n > 0 & $1 = A |^ n;
    reconsider M = { B: P[B] } as Subset-Family of E^omega from DOMAIN_1:sch 7;
    union M is Subset of E^omega;
    hence thesis;
  end;
end;

:: Positive Closure
:: Properties of +

theorem Th48:
  x in A+ iff ex n st n > 0 & x in A |^ n
proof
  thus x in A+ implies ex n st n > 0 & x in A |^ n
  proof
    defpred P[set] means ex n st n > 0 & $1 = A |^ n;
    assume x in A+;
    then consider X such that
A1: x in X and
A2: X in { B: ex n st n > 0 & B = A |^ n } by TARSKI:def 4;
A3: X in { B: P[B] } by A2;
    P[X] from CARD_FIL:sch 1(A3);
    hence thesis by A1;
  end;
  given n such that
A4: n > 0 and
A5: x in A |^ n;
  defpred P[set] means ex n st n > 0 & $1 = A |^ n;
  consider B such that
A6: x in B and
A7: P[B] by A4,A5;
  reconsider A = { C : P[C] } as Subset-Family of E^omega from DOMAIN_1:sch 7;
  B in A by A7;
  hence thesis by A6,TARSKI:def 4;
end;

theorem Th49:
  n > 0 implies A |^ n c= A+
proof
  assume n > 0;
  then for x holds x in A |^ n implies x in A+ by Th48;
  hence thesis by TARSKI:def 3;
end;

theorem Th50:
  A+ = A |^.. 1
proof
A1: now
    let x;
    assume x in A+;
    then consider k such that
A2: 0 < k and
A3: x in A |^ k by Th48;
    0 + 1 <= k by A2,NAT_1:13;
    hence x in A |^.. 1 by A3,Th2;
  end;
  now
    let x;
    assume x in A |^.. 1;
    then ex k st 1 <= k & x in A |^ k by Th2;
    hence x in A+ by Th48;
  end;
  hence thesis by A1,TARSKI:1;
end;

theorem
  A+ = {} iff A = {}
proof
  A+ = A |^.. 1 by Th50;
  hence thesis by Th4;
end;

theorem Th52:
  A+ = (A*) ^^ A
proof
  A* ^^ A = A |^.. 1 by Th30;
  hence thesis by Th50;
end;

theorem Th53:
  A* = {<%>E} \/ (A+)
proof
  thus A* = {<%>E} \/ ((A*) ^^ A) by FLANG_1:56
    .= {<%>E} \/ (A+) by Th52;
end;

theorem
  A+ = A |^ (1, n) \/ A |^.. (n + 1)
proof
A1: 0 + 1 <= n + 1 by XREAL_1:7;
  thus A+ = A |^.. 1 by Th50
    .= A |^ (1, n) \/ A |^.. (n + 1) by A1,Th7;
end;

theorem Th55:
  A+ c= A*
proof
  A |^.. 1 c= A* by Th9;
  hence thesis by Th50;
end;

theorem Th56:
  <%>E in A+ iff <%>E in A
proof
  A+ = A |^.. 1 by Th50;
  hence thesis by Th10;
end;

theorem Th57:
  A+ = A* iff <%>E in A
proof
  thus A+ = A* implies <%>E in A
  proof
    assume A+ = A*;
    then <%>E in A+ by FLANG_1:48;
    hence thesis by Th56;
  end;
  assume <%>E in A;
  then A* = (A*) ^^ A by FLANG_1:54;
  hence thesis by Th52;
end;

theorem Th58:
  A c= B implies A+ c= B+
proof
  assume A c= B;
  then A |^.. 1 c= B |^.. 1 by Th13;
  then A+ c= B |^.. 1 by Th50;
  hence thesis by Th50;
end;

theorem Th59:
  A c= A+
proof
  A |^ 1 c= A+ by Th49;
  hence thesis by FLANG_1:25;
end;

theorem Th60:
  (A*)+ = A* & (A+)* = A*
proof
A1: A* c= (A+)* by Th59,FLANG_1:61;
  now
    let x;
    assume x in (A*)+;
    then consider k such that
    0 < k and
A2: x in (A*) |^ k by Th48;
    (A*) |^ k c= A* by FLANG_1:65;
    hence x in A* by A2;
  end;
  then
A3: (A*)+ c= A* by TARSKI:def 3;
  now
    let x;
    assume x in (A+)*;
    then consider k such that
A4: x in (A+) |^ k by FLANG_1:41;
    (A+) |^ k c= A* by Th55,FLANG_1:59;
    hence x in A* by A4;
  end;
  then
A5: (A+)* c= A* by TARSKI:def 3;
  A* c= (A*)+ by Th59;
  hence thesis by A1,A3,A5,XBOOLE_0:def 10;
end;

theorem Th61:
  A c= B* implies A+ c= B*
proof
  assume A c= B*;
  then A+ c= (B*)+ by Th58;
  hence thesis by Th60;
end;

theorem
  (A+)+ = A+
proof
  now
    let x;
    assume that
A1: x in (A+)+;
    per cases;
    suppose
      x = <%>E;
      hence x in A+ by A1,Th56;
    end;
    suppose
A2:   x <> <%>E;
      (A+)+ c= A* by Th55,Th61;
      then x in A* by A1;
      then
A3:   x in (A+) \/ {<%>E} by Th53;
      not x in {<%>E} by A2,TARSKI:def 1;
      hence x in A+ by A3,XBOOLE_0:def 3;
    end;
  end;
  then
A4: (A+)+ c= A+ by TARSKI:def 3;
  A+ c= (A+)+ by Th59;
  hence thesis by A4,XBOOLE_0:def 10;
end;

theorem
  x in A & x <> <%>E implies A+ <> {<%>E}
proof
  assume that
A1: x in A and
A2: x <> <%>E;
  A+ = A |^.. 1 by Th50;
  hence thesis by A1,A2,Th14;
end;

theorem
  A+ = {<%>E} iff A = {<%>E}
proof
  A+ = A |^.. 1 by Th50;
  hence thesis by Th15;
end;

theorem
  (A+)? = A* & (A?)+ = A*
proof
  thus (A+)? = {<%>E} \/ (A+) by FLANG_2:76
    .= A* by Th53;
  <%>E in A? by FLANG_2:78;
  then (A?)+ = (A?)* by Th57;
  hence (A?)+ = A* by FLANG_2:85;
end;

theorem Th66:
  a in C+ & b in C+ implies a ^ b in C+
proof
  assume that
A1: a in C+ and
A2: b in C+;
  consider l such that
  l > 0 and
A3: b in C |^ l by A2,Th48;
  consider k such that
A4: k > 0 and
A5: a in C |^ k by A1,Th48;
  a ^ b in C |^ (k + l) by A5,A3,FLANG_1:40;
  hence thesis by A4,Th48;
end;

theorem
  A c= C+ & B c= C+ implies A ^^ B c= C+
proof
  assume that
A1: A c= C+ and
A2: B c= C+;
  now
    let x;
    assume x in A ^^ B;
    then ex a, b st a in A & b in B & x = a ^ b by FLANG_1:def 1;
    hence x in C+ by A1,A2,Th66;
  end;
  hence thesis by TARSKI:def 3;
end;

theorem
  A ^^ A c= A+
proof
  A ^^ A = A |^ 2 by FLANG_1:26;
  hence thesis by Th49;
end;

theorem
  A+ = {x} implies x = <%>E
proof
  assume that
A1: A+ = {x} and
A2: x <> <%>E;
  A |^.. 1 = {x} by A1,Th50;
  hence thesis by A2,Th38;
end;

theorem
  A ^^ (A+) = (A+) ^^ A
proof
  thus A ^^ (A+) = A ^^ (A |^.. 1) by Th50
    .= (A |^.. 1) ^^ A by Th23
    .= A+ ^^ A by Th50;
end;

theorem
  (A |^ k) ^^ (A+) = (A+) ^^ (A |^ k)
proof
  thus (A |^ k) ^^ (A+) = (A |^ k) ^^ (A |^.. 1) by Th50
    .= (A |^.. 1) ^^ (A |^ k) by Th24
    .= A+ ^^ (A |^ k) by Th50;
end;

theorem Th72:
  (A |^ (m, n)) ^^ (A+) = A+ ^^ (A |^ (m, n))
proof
  thus (A |^ (m, n)) ^^ (A+) = (A |^ (m, n)) ^^ (A |^.. 1) by Th50
    .= (A |^.. 1) ^^ (A |^ (m, n)) by Th25
    .= A+ ^^ (A |^ (m, n)) by Th50;
end;

theorem
  <%>E in B implies A c= A ^^ (B+) & A c= (B+) ^^ A
proof
  assume <%>E in B;
  then B+ = B* by Th57;
  hence thesis by FLANG_2:18;
end;

theorem
  A+ ^^ (A+) = A |^.. 2
proof
  thus A+ ^^ (A+) = A |^.. 1 ^^ (A+) by Th50
    .= A |^.. 1 ^^ (A |^.. 1) by Th50
    .= A |^.. (1 + 1) by Th18
    .= A |^.. 2;
end;

theorem Th75:
  A+ ^^ (A |^ k) = A |^.. (k + 1)
proof
  thus A+ ^^ (A |^ k) = (A |^.. 1) ^^ (A |^ k) by Th50
    .= A |^.. (k + 1) by Th22;
end;

theorem
  A+ ^^ A = A |^.. 2
proof
  A+ ^^ A = A+ ^^ (A |^ 1) by FLANG_1:25
    .= A |^.. (1 + 1) by Th75;
  hence thesis;
end;

theorem
  k <= l implies A+ ^^ (A |^ (k, l)) = A |^.. (k + 1)
proof
  assume k <= l;
  then (A |^.. 1) ^^ (A |^ (k, l)) = A |^.. (1 + k) by Th33;
  hence thesis by Th50;
end;

theorem
  A c= B+ & n > 0 implies A |^ n c= B+
proof
  assume that
A1: A c= B+ and
A2: n > 0;
  A c= B |^.. 1 by A1,Th50;
  then A |^ n c= B |^.. 1 by A2,Th28;
  hence thesis by Th50;
end;

theorem
  A+ ^^ (A?) = A? ^^ (A+)
proof
  thus A+ ^^ (A?) = A+ ^^ (A |^ (0, 1)) by FLANG_2:79
    .= A |^ (0, 1) ^^ (A+) by Th72
    .= A? ^^ (A+) by FLANG_2:79;
end;

theorem
  A+ ^^ (A?) = A+
proof
  thus A+ ^^ (A?) = A |^.. 1 ^^ (A?) by Th50
    .= A |^.. 1 by Th41
    .= A+ by Th50;
end;

theorem
  A? c= A+ iff <%>E in A
proof
  A+ = A |^.. 1 by Th50;
  hence thesis by Th40;
end;

theorem
  A c= B+ implies A+ c= B+
proof
  assume A c= B+;
  then A c= B |^.. 1 by Th50;
  then A |^.. 1 c= B |^.. 1 by Th29;
  then A+ c= B |^.. 1 by Th50;
  hence thesis by Th50;
end;

theorem
  A c= B+ implies B+ = (B \/ A)+
proof
  assume A c= B+;
  then A c= B |^.. 1 by Th50;
  then B |^.. 1 = (B \/ A) |^.. 1 by Th47;
  then B |^.. 1 = (B \/ A)+ by Th50;
  hence thesis by Th50;
end;

theorem
  n > 0 implies A |^.. n c= A+
proof
  assume
A1: n > 0;
  let x;
  assume x in A |^.. n;
  then ex k st k >= n & x in A |^ k by Th2;
  hence thesis by A1,Th48;
end;

theorem
  m > 0 implies A |^ (m, n) c= A+
proof
  assume
A1: m > 0;
  let x;
  assume x in A |^ (m, n);
  then ex k st m <= k & k <= n & x in A |^ k by FLANG_2:19;
  hence thesis by A1,Th48;
end;

theorem Th86:
  A* ^^ (A+) = A+ ^^ (A*)
proof
  thus A* ^^ (A+) = A* ^^ (A |^.. 1) by Th50
    .= (A |^.. 1) ^^ (A*) by Th32
    .= A+ ^^ (A*) by Th50;
end;

theorem Th87:
  A+ |^ k c= A |^.. k
proof
  per cases;
  suppose
    k > 0;
    then (A |^.. 1) |^ k c= A |^.. (1 * k) by Th19;
    hence thesis by Th50;
  end;
  suppose
A1: k = 0;
    A |^.. 0 = A* by Th11;
    then
A2: <%>E in A |^.. 0 by FLANG_1:48;
    A+ |^ k = {<%>E} by A1,FLANG_1:24;
    hence thesis by A1,A2,ZFMISC_1:31;
  end;
end;

theorem
  A+ |^ (m, n) c= A |^.. m
proof
  let x;
  assume x in A+ |^ (m, n);
  then consider k such that
A1: m <= k and
  k <= n and
A2: x in A+ |^ k by FLANG_2:19;
  A+ |^ k c= A |^.. k by Th87;
  then
A3: x in A |^.. k by A2;
  A |^.. k c= A |^.. m by A1,Th5;
  hence thesis by A3;
end;

theorem
  A c= B+ & n > 0 implies A |^.. n c= B+
proof
  assume that
A1: A c= B+ and
A2: n > 0;
  A c= B |^.. 1 by A1,Th50;
  then A |^.. n c= B |^.. 1 by A2,Th29;
  hence thesis by Th50;
end;

theorem Th90:
  A+ ^^ (A |^.. k) = A |^.. (k + 1)
proof
  thus A+ ^^ (A |^.. k) = (A |^.. 1) ^^ (A |^.. k) by Th50
    .= A |^.. (k + 1) by Th18;
end;

theorem
  A+ ^^ (A |^.. k) = A |^.. k ^^ (A+)
proof
  thus A+ ^^ (A |^.. k) = A |^.. (k + 1) by Th90
    .= (A |^.. k) ^^ (A |^.. 1) by Th18
    .= A |^.. k ^^ (A+) by Th50;
end;

theorem Th92:
  A+ ^^ (A*) = A+
proof
  thus A+ ^^ (A*) = (A |^.. 1) ^^ (A*) by Th50
    .= A |^.. 1 by Th17
    .= A+ by Th50;
end;

theorem
  B c= A* implies A+ ^^ B c= A+ & B ^^ (A+) c= A+
proof
  assume
A1: B c= A*;
  then B ^^ (A+) c= A* ^^ (A+) by FLANG_1:17;
  then
A2: B ^^ (A+) c= A+ ^^ (A*) by Th86;
  A+ ^^ B c= A+ ^^ (A*) by A1,FLANG_1:17;
  hence thesis by A2,Th92;
end;

theorem
  (A /\ B)+ c= (A+) /\ (B+)
proof
A1: A+ = A |^.. 1 by Th50;
A2: B+ = B |^.. 1 by Th50;
  (A /\ B)+ = (A /\ B) |^.. 1 by Th50;
  hence thesis by A1,A2,Th44;
end;

theorem
  (A+) \/ (B+) c= (A \/ B)+
proof
A1: A+ = A |^.. 1 by Th50;
A2: B+ = B |^.. 1 by Th50;
  (A \/ B)+ = (A \/ B) |^.. 1 by Th50;
  hence thesis by A1,A2,Th45;
end;

theorem
  <%x%> in A+ iff <%x%> in A
proof
  A+ = A |^.. 1 by Th50;
  hence thesis by Th46;
end;