Caves Travel Diving Graphics Mizar Texts Cuisine Lemkov Contact Map RSS Polski
Trybiks' Dive Mizar Articles Regular Expression Quantifiers - m to n Occurrences YAC Software
  Back

Mizar

Eddie

Articles

Equivalence of Deterministic and Epsilon Nondeterministic Automata

Labelled State Transition Systems

Regular Expression Quantifiers - at least m Occurrences

String Rewriting Systems

Regular Expression Quantifiers - m to n Occurrences

Formal Languages- Concatenation and Closure

Boolean Properties of Sets

Homomorphisms and Isomorphisms of Groups; Quotient Group

Integers

Mizar-MSE Syntax

Regular Expression Quantifiers - m to n Occurrences
This article includes proofs of several facts that are supplemental to the theorems proved in [1]. Next, it builds upon that theory to extend the framework for proving facts about formal languages in general and regular expression operators in particular. In this article, two quantifiers are defined and their properties are shown: m to n occurrences (or the union of a range of powers) and optional occurrence. Although optional occurrence is a special case of the previous operator (0 to 1 occurrences), it is often defined in regex applications as a separate operator - hence its explicit definition and properties in the article. Notation and terminology were taken from [2].

Sections:
  • Preliminaries
  • Addenda to FLANG_1
  • Union of a Range of Powers
  • Optional Occurrence
Bibliography: Mizar Mathematical Library identifier: FLANG_2.
Abstract in PDF: here.
Motorola Software Group, 2007.

Files: Abstract
:: Regular Expression Quantifiers -- $m$ to $n$ Occurrences
::  by Micha{\l} Trybulec
::
:: Received June 6, 2007
:: Copyright (c) 2007 Association of Mizar Users

environ

 vocabularies BOOLE, FINSEQ_1, TARSKI, ALGSEQ_1, ARYTM_1, AFINSQ_1, MEASURE6,
      GROUP_1, ARYTM, SETFAM_1, MODAL_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XCMPLX_0, NAT_1,
      DOMAIN_1, FUNCT_1, RELSET_1, FUNCT_2, ORDINAL1, SETFAM_1, XREAL_0,
      XXREAL_0, AFINSQ_1, CATALAN2, FLANG_1;
 constructors XXREAL_0, NAT_1, XREAL_0, CATALAN2, FLANG_1;
 registrations SUBSET_1, RELSET_1, NAT_1, ORDINAL1, AFINSQ_1, XREAL_0,
      XBOOLE_0, RELAT_1, FUNCT_1, ARYTM_3, XXREAL_0;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
 definitions TARSKI;
 theorems AFINSQ_1, NAT_1, REAL_1, SUBSET_1, TARSKI, XBOOLE_0, XBOOLE_1,
      XREAL_1, ZFMISC_1, FLANG_1, XXREAL_0;
 schemes CARD_FIL, DOMAIN_1, NAT_1;

begin

 reserve E, x, y, X, Y, Z for set;
 reserve A, B, C, D for Subset of E^omega;
 reserve a, a1, a2, b, c, d for Element of E^omega;
 reserve e for Element of E;
 reserve i, j, k, l, kl, m, n, mn, n1, n2 for Nat;
 reserve p, q, r, r1, r2 for real number;

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Preliminaries - Numbers:
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

theorem :: FLANG_2:1
m + k <= i & i <= n + k implies
  ex mn st mn + k = i & m <= mn & mn <= n;

theorem :: FLANG_2:2
m <= n & k <= l & m + k <= i & i <= n + l implies
  ex mn, kl st mn + kl = i & m <= mn & mn <= n & k <= kl & kl <= l;

theorem :: FLANG_2:3
m < n implies ex k st m + k = n & k > 0;

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Preliminaries - Sequences:
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

theorem :: FLANG_2:4
a ^ b = a or b ^ a = a implies b = {};

begin

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Addenda - FLANG_1:
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

theorem :: FLANG_2:5
(x in A or x in B) & x <> <%>E implies A ^^ B <> {<%>E};

theorem :: FLANG_2:6
<%x%> in A ^^ B iff <%>E in A & <%x%> in B or <%x%> in A & <%>E in B;

theorem :: FLANG_2:7
x in A & x <> <%>E & n > 0 implies A |^ n <> {<%>E};

theorem :: FLANG_2:8
<%>E in A |^ n iff n = 0 or <%>E in A;

theorem :: FLANG_2:9
<%x%> in A |^ n iff <%x%> in A & ((<%>E in A & n > 1) or n = 1);

theorem :: FLANG_2:10
m <> n & A |^ m = {x} & A |^ n = {x} implies x = <%>E;

theorem :: FLANG_2:11
(A |^ m) |^ n = (A |^ n) |^ m;

theorem :: FLANG_2:12
(A |^ m) ^^ (A |^ n) = (A |^ n) ^^ (A |^ m);

theorem :: FLANG_2:13
<%>E in B implies A c= A ^^ (B |^ l) & A c= (B |^ l) ^^ A;

theorem :: FLANG_2:14
A c= C |^ k & B c= C |^ l implies A ^^ B c= C |^ (k + l);

theorem :: FLANG_2:15
x in A & x <> <%>E implies A* <> {<%>E};

theorem :: FLANG_2:16
<%>E in A & n > 0 implies (A |^ n)* = A*;

theorem :: FLANG_2:17
<%>E in A implies (A |^ n)* = (A*) |^ n;

theorem :: FLANG_2:18
A c= A ^^ (B*) & A c= (B*) ^^ A;

begin

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Union of a Range of Powers
:: Definition of |^ (n, m)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

definition
  let E, A;
  let m, n;
  func A |^ (m, n) -> Subset of E^omega equals
:: FLANG_2:def 1
    union { B: ex k st m <= k & k <= n & B = A |^ k };
end;

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Union of a Range of Powers
:: Properties of |^ (n, m)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

theorem :: FLANG_2:19
x in A |^ (m, n) iff ex k st m <= k & k <= n & x in A |^ k;

theorem :: FLANG_2:20
m <= k & k <= n implies A |^ k c= A |^ (m, n);

theorem :: FLANG_2:21
A |^ (m, n) = {} iff m > n or (m > 0 & A = {});

theorem :: FLANG_2:22
A |^ (m, m) = A |^ m;

theorem :: FLANG_2:23
m <= k & l <= n implies A |^ (k, l) c= A |^ (m, n);

theorem :: FLANG_2:24
m <= k & k <= n implies A |^ (m, n) = A |^ (m, k) \/ A |^ (k, n);

theorem :: FLANG_2:25
m <= k & k <= n implies A |^ (m, n) = A |^ (m, k) \/ A |^ (k + 1, n);

theorem :: FLANG_2:26
m <= n + 1 implies A |^ (m, n + 1) = A |^ (m, n) \/ (A |^ (n + 1));

theorem :: FLANG_2:27
m <= n implies A |^ (m, n) = A |^ m \/ A |^ (m + 1, n);

theorem :: FLANG_2:28
A |^ (n, n + 1) = A |^ n \/ A |^ (n + 1);

theorem :: FLANG_2:29
A c= B implies A |^ (m, n) c= B |^ (m, n);

theorem :: FLANG_2:30
x in A & x <> <%>E & (m > 0 or n > 0) implies A |^ (m, n) <> {<%>E};

theorem :: FLANG_2:31
A |^ (m, n) = {<%>E} iff
  (m <= n & A = {<%>E}) or (m = 0 & n = 0) or (m = 0 & A = {});

theorem :: FLANG_2:32
A |^ (m, n) c= A*;

theorem :: FLANG_2:33
<%>E in A |^ (m, n) iff m = 0 or (m <= n & <%>E in A);

theorem :: FLANG_2:34
<%>E in A & m <= n implies A |^ (m, n) = A |^ n;

theorem :: FLANG_2:35
A |^ (m, n) ^^ (A |^ k) = (A |^ k) ^^ (A |^ (m, n));

theorem :: FLANG_2:36
(A |^ (m, n)) ^^ A = A ^^ (A |^ (m, n));

theorem :: FLANG_2:37
m <= n & k <= l implies (A |^ (m, n)) ^^ (A |^ (k, l)) = A |^ (m + k, n + l);

theorem :: FLANG_2:38
A |^ (m + 1, n + 1) = (A |^ (m, n)) ^^ A;

theorem :: FLANG_2:39
(A |^ (m, n)) ^^ (A |^ (k, l)) = (A |^ (k, l)) ^^ (A |^ (m, n));

theorem :: FLANG_2:40
(A |^ (m, n)) |^ k = A |^ (m * k, n * k);

theorem :: FLANG_2:41
(A |^ (k + 1)) |^ (m, n) c= ((A |^ k) |^ (m, n)) ^^ (A |^ (m, n));

theorem :: FLANG_2:42
(A |^ k) |^ (m, n) c= A |^ (k * m, k * n);

theorem :: FLANG_2:43
(A |^ k) |^ (m, n) c= (A |^ (m, n)) |^ k;

theorem :: FLANG_2:44
(A |^ (k + l)) |^ (m, n) c= ((A |^ k) |^ (m, n)) ^^ ((A |^ l) |^ (m, n));

theorem :: FLANG_2:45
A |^ (0, 0) = {<%>E};

theorem :: FLANG_2:46
A |^ (0, 1) = {<%>E} \/ A;

theorem :: FLANG_2:47
A |^ (1, 1) = A;

theorem :: FLANG_2:48
A |^ (0, 2) = {<%>E} \/ A \/ (A ^^ A);

theorem :: FLANG_2:49
A |^ (1, 2) = A \/ (A ^^ A);

theorem :: FLANG_2:50
A |^ (2, 2) = A ^^ A;

theorem :: FLANG_2:51
m > 0 & m <> n & A |^ (m, n) = {x} implies
  for mn st m <= mn & mn <= n holds A |^ mn = {x};

theorem :: FLANG_2:52
m <> n & A |^ (m, n) = {x} implies x = <%>E;

theorem :: FLANG_2:53
<%x%> in A |^ (m, n) iff
  <%x%> in A & m <= n & ((<%>E in A & (n > 0)) or (m <= 1 & 1 <= n));

theorem :: FLANG_2:54
(A /\ B) |^ (m, n) c= (A |^ (m, n)) /\ (B |^ (m, n));

theorem :: FLANG_2:55
(A |^ (m, n)) \/ (B |^ (m, n)) c= (A \/ B) |^ (m, n);

theorem :: FLANG_2:56
(A |^ (m, n)) |^ (k, l) c= A |^ (m * k, n * l);

theorem :: FLANG_2:57
m <= n & <%>E in B implies A c= A ^^ (B |^ (m, n)) & A c= (B |^ (m, n)) ^^ A;

theorem :: FLANG_2:58
m <= n & k <= l & A c= C |^ (m, n) & B c= C |^ (k, l) implies
  A ^^ B c= C |^ (m + k, n + l);

theorem :: FLANG_2:59
(A |^ (m, n))* c= A*;

theorem :: FLANG_2:60
(A*) |^ (m, n) c= A*;

theorem :: FLANG_2:61
m <= n & n > 0 implies (A*) |^ (m, n) = A*;

theorem :: FLANG_2:62
m <= n & n > 0 & <%>E in A implies (A |^ (m, n))* = A*;

theorem :: FLANG_2:63
m <= n & <%>E in A implies (A |^ (m, n))* = (A*) |^ (m, n);

theorem :: FLANG_2:64
A c= B* implies A |^ (m, n) c= B*;

theorem :: FLANG_2:65
A c= B* implies B* = (B \/ (A |^ (m, n)))*;

theorem :: FLANG_2:66
A |^ (m, n) ^^ (A*) = A* ^^ (A |^ (m, n));

theorem :: FLANG_2:67
<%>E in A & m <= n implies A* = A* ^^ (A |^ (m, n));

theorem :: FLANG_2:68
A |^ (m, n) |^ k c= A*;

theorem :: FLANG_2:69
A |^ k |^ (m, n) c= A*;

theorem :: FLANG_2:70
m <= n implies (A |^ m)* c= (A |^ (m, n))*;

theorem :: FLANG_2:71
(A |^ (m, n)) |^ (k, l) c= A*;

theorem :: FLANG_2:72
<%>E in A & k <= n & l <= n implies A |^ (k, n) = A |^ (l, n);

begin

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Optional Occurrence
:: Definition of ?
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

definition
  let E, A;
  func A? -> Subset of E^omega equals
:: FLANG_2:def 2
    union { B: ex k st k <= 1 & B = A |^ k };
end;

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Optional Occurrence
:: Properties of ?
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

theorem :: FLANG_2:73
x in A? iff ex k st k <= 1 & x in A |^ k;

theorem :: FLANG_2:74
n <= 1 implies A |^ n c= A?;

theorem :: FLANG_2:75
A? = (A |^ 0) \/ (A |^ 1);

theorem :: FLANG_2:76
A? = {<%>E} \/ A;

theorem :: FLANG_2:77
A c= A?;

theorem :: FLANG_2:78
x in A? iff x = <%>E or x in A;

theorem :: FLANG_2:79
A? = A |^ (0, 1);

theorem :: FLANG_2:80
A? = A iff <%>E in A;

registration let E, A;
  cluster A? -> non empty;
end;

theorem :: FLANG_2:81
A?? = A?;

theorem :: FLANG_2:82
A c= B implies A? c= B?;

theorem :: FLANG_2:83
x in A & x <> <%>E implies A? <> {<%>E};

theorem :: FLANG_2:84
A? = {<%>E} iff A = {} or A = {<%>E};

theorem :: FLANG_2:85
(A*)? = A* & (A?)* = A*;

theorem :: FLANG_2:86
A? c= A*;

theorem :: FLANG_2:87
(A /\ B)? = (A?) /\ (B?);

theorem :: FLANG_2:88
(A?) \/ (B?) = (A \/ B)?;

theorem :: FLANG_2:89
A? = {x} implies x = <%>E;

theorem :: FLANG_2:90
<%x%> in A? iff <%x%> in A;

theorem :: FLANG_2:91
(A?) ^^ A = A ^^ (A?);

theorem :: FLANG_2:92
(A?) ^^ A = A |^ (1, 2);

theorem :: FLANG_2:93
(A?) ^^ (A?) = A |^ (0, 2);

theorem :: FLANG_2:94
(A?) |^ k = (A?) |^ (0, k);

theorem :: FLANG_2:95
(A?) |^ k = A |^ (0, k);

theorem :: FLANG_2:96
m <= n implies A? |^ (m, n) = A? |^ (0, n);

theorem :: FLANG_2:97
A? |^ (0, n) = A |^ (0, n);

theorem :: FLANG_2:98
m <= n implies A? |^ (m, n) = A |^ (0, n);

theorem :: FLANG_2:99
(A |^ (1, n))? = A |^ (0, n);

theorem :: FLANG_2:100
<%>E in A & <%>E in B implies A? c= A ^^ B & A? c= B ^^ A;

theorem :: FLANG_2:101
A c= A ^^ (B?) & A c= (B?) ^^ A;

theorem :: FLANG_2:102
A c= C? & B c= C? implies A ^^ B c= C |^ (0, 2);

theorem :: FLANG_2:103
<%>E in A & n > 0 implies A? c= A |^ n;

theorem :: FLANG_2:104
(A?) ^^ (A |^ k) = (A |^ k) ^^ (A?);

theorem :: FLANG_2:105
A c= B* implies A? c= B*;

theorem :: FLANG_2:106
A c= B* implies B* = (B \/ (A?))*;

theorem :: FLANG_2:107
A? ^^ (A*) = A* ^^ (A?);

theorem :: FLANG_2:108
A? ^^ (A*) = A*;

theorem :: FLANG_2:109
A? |^ k c= A*;

theorem :: FLANG_2:110
(A |^ k)? c= A*;

theorem :: FLANG_2:111
(A?) ^^ (A |^ (m, n)) = (A |^ (m, n)) ^^ (A?);

theorem :: FLANG_2:112
(A?) ^^ (A |^ k) = A |^ (k, k + 1);

theorem :: FLANG_2:113
A? |^ (m, n) c= A*;

theorem :: FLANG_2:114
(A |^ (m, n))? c= A*;

theorem :: FLANG_2:115
A? = (A \ {<%>E})?;

theorem :: FLANG_2:116
A c= B? implies A? c= B?;

theorem :: FLANG_2:117
A c= B? implies B? = (B \/ A)?;


Top

Full article
:: Regular Expression Quantifiers -- $m$ to $n$ Occurrences
::  by Micha{\l} Trybulec
:: 
:: Received June 6, 2007
:: Copyright (c) 2007 Association of Mizar Users

environ

 vocabularies BOOLE, FINSEQ_1, TARSKI, ALGSEQ_1, ARYTM_1, AFINSQ_1, MEASURE6,
      GROUP_1, ARYTM, SETFAM_1, MODAL_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XCMPLX_0, NAT_1,
      DOMAIN_1, FUNCT_1, RELSET_1, FUNCT_2, ORDINAL1, SETFAM_1, XREAL_0,
      XXREAL_0, AFINSQ_1, CATALAN2, FLANG_1;
 constructors XXREAL_0, NAT_1, XREAL_0, CATALAN2, FLANG_1;
 registrations SUBSET_1, RELSET_1, NAT_1, ORDINAL1, AFINSQ_1, XREAL_0,
      XBOOLE_0, RELAT_1, FUNCT_1, ARYTM_3, XXREAL_0;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
 definitions TARSKI;
 theorems AFINSQ_1, NAT_1, REAL_1, SUBSET_1, TARSKI, XBOOLE_0, XBOOLE_1,
      XREAL_1, ZFMISC_1, FLANG_1, XXREAL_0;
 schemes CARD_FIL, DOMAIN_1, NAT_1;

begin

 reserve E, x, y, X, Y, Z for set;
 reserve A, B, C, D for Subset of E^omega;
 reserve a, a1, a2, b, c, d for Element of E^omega;
 reserve e for Element of E;
 reserve i, j, k, l, kl, m, n, mn, n1, n2 for Nat;
 reserve p, q, r, r1, r2 for real number;

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Preliminaries - Numbers:
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

theorem LmNum19:
m + k <= i & i <= n + k implies
  ex mn st mn + k = i & m <= mn & mn <= n
proof
  assume 
A:  m + k <= i & i <= n + k;
  then m + k <= m + i by XREAL_1:40;  
  then k <= i by XREAL_1:8;
  then reconsider mn = i - k as Nat by NAT_1:21;
  take mn;
  thus mn + k = i;
  m + k <= mn + k & mn + k <= n + k by A;
  hence m <= mn & mn <= n by XREAL_1:8;
end;  

theorem LmNum20:
m <= n & k <= l & m + k <= i & i <= n + l implies
  ex mn, kl st mn + kl = i & m <= mn & mn <= n & k <= kl & kl <= l
proof
  assume 
A:  m <= n & k <= l & m + k <= i & i <= n + l;
  per cases;
  suppose i <= n + k;
    then consider mn such that
B2:   mn + k = i & m <= mn & mn <= n by A, LmNum19;
    take mn, k;
    thus mn + k = i & m <= mn & mn <= n by B2;
    thus k <= k & k <= l by A;
  end;
  suppose i > n + k;
    then consider kl such that
B2:   kl + n = i & k <= kl & kl <= l by A, LmNum19;
    take n, kl;
    thus n + kl = i & m <= n & n <= n by A, B2;
    thus k <= kl & kl <= l by B2;  
  end;
end;  

theorem LmNum30:
m < n implies ex k st m + k = n & k > 0
proof
  assume 
A:  m < n;
  then consider k such that
B:  m + k = n by NAT_1:10;
  m - m < n - m by A, XREAL_1:16;
  hence thesis by B;
end;

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Preliminaries - Sequences:
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

theorem LmSeq20:
a ^ b = a or b ^ a = a implies b = {}
proof
  assume 
A:  a ^ b = a or b ^ a = a;
  per cases by A;
  suppose a ^ b = a;
    then len(a ^ b) = len(a) + len(b) & len(a ^ b) = len(a) by AFINSQ_1:20;
    hence thesis by AFINSQ_1:18; 
  end;
  suppose b ^ a = a;
    then len(b ^ a) = len(b) + len(a) & len(b ^ a) = len(a) by AFINSQ_1:20;
    hence thesis by AFINSQ_1:18; 
  end;
end;

begin

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Addenda - FLANG_1:
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

theorem 
(x in A or x in B) & x <> <%>E implies A ^^ B <> {<%>E}
proof
  assume (x in A or x in B) & x <> <%>E;
  then A <> {<%>E} or B <> {<%>E} by TARSKI:def 1;
  hence thesis by FLANG_1:15;
end;

theorem 
<%x%> in A ^^ B iff <%>E in A & <%x%> in B or <%x%> in A & <%>E in B
proof
  thus <%x%> in A ^^ B implies <%>E in A & <%x%> in B or <%x%> in A & <%>E in B
  proof
    assume <%x%> in A ^^ B;
    then consider a, b such that
A:    a in A & b in B & <%x%> = a ^ b by FLANG_1:def 1;
    thus thesis by A, FLANG_1:4; 
  end;
  assume 
B:  <%>E in A & <%x%> in B or <%x%> in A & <%>E in B;
  <%>E ^ <%x%> = <%x%> & <%x%> ^ <%>E = <%x%> by AFINSQ_1:32;
  hence thesis by B, FLANG_1:def 1;
end;

theorem LmLang20:
x in A & x <> <%>E & n > 0 implies A |^ n <> {<%>E}
proof
  assume that 
A1: x in A & x <> <%>E and
A2: n > 0;
  A <> {<%>E} by A1, TARSKI:def 1;
  hence thesis by A2, FLANG_1:30;
end;

theorem 
<%>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 that
A1:   <%>E in A |^ n and
A2:   n <> 0 & not <%>E in A;
    n > 0 by A2;
    hence contradiction by A1, A2, FLANG_1:32;
  end;
  assume 
B:  n = 0 or <%>E in A;
  per cases by B;
  suppose n = 0;
    then A |^ n = {<%>E} by FLANG_1:30;
    hence thesis by ZFMISC_1:37;
  end;
  suppose <%>E in A;
    hence thesis by FLANG_1:31;
  end;
end;

theorem LmLang31:
<%x%> in A |^ n iff <%x%> in A & ((<%>E in A & n > 1) or n = 1)
proof
  thus <%x%> in A |^ n implies <%x%> in A & ((<%>E in A & n > 1) or n = 1)
  proof
    assume 
A1:   <%x%> in A |^ n;
    A |^ n c= A* by FLANG_1:43;
    hence <%x%> in A by A1, FLANG_1:73;
    assume 
A2:   (not <%>E in A or n <= 1) & n <> 1;
    per cases by A2;
    suppose 
A3:   not <%>E in A & n <> 1;
      per cases by A3, NAT_1:26;
      suppose n = 0;
        then A |^ n = {<%>E} by FLANG_1:25;
        hence contradiction by A1, TARSKI:def 1;
      end;
      suppose 
A3a:    n > 1;
        then consider m such that
A3b:      m + 1 = n by NAT_1:6;
        <%x%> in (A |^ m) ^^ A by A1, A3b, FLANG_1:24;
        then consider a, b such that
A3c:      a in (A |^ m) & b in A & <%x%> = a ^ b by FLANG_1:def 1;
        per cases by FLANG_1:4, A3c;
        suppose 
A3d:      a = <%>E & b = <%x%>;
          m + 1 > 0 + 1 by A3a, A3b;
          then m > 0 by XREAL_1:8;
          hence contradiction by A3, A3c, A3d, FLANG_1:32;
        end;
        suppose b = <%>E & a = <%x%>;
          hence contradiction by A3c, A3;
        end;
      end;
    end;
    suppose n <= 1 & n <> 1;
      then n = 0 by NAT_1:26;
      then A |^ n = {<%>E} by FLANG_1:25;
      hence contradiction by A1, TARSKI:def 1;
    end;
  end;
  assume that
B1: <%x%> in A and 
B2: (<%>E in A & n > 1) or n = 1;
  per cases by B2;
  suppose <%>E in A & n > 1;
    then A c= A |^ n by FLANG_1:36;
    hence thesis by B1;
  end;
  suppose n = 1;
    hence thesis by B1, FLANG_1:26;
  end;   
end;

theorem LmLang32:
m <> n & A |^ m = {x} & A |^ n = {x} implies x = <%>E
proof
  assume
A:  m <> n & A |^ m = {x} & A |^ n = {x};
A1:
  x in A |^ m & x in A |^ n by A, TARSKI:def 1;
  per cases by A, REAL_1:def 5;
  suppose m > n;
    then consider k such that
B:    n + k = m & k > 0 by LmNum30;
    (A |^ n) ^^ (A |^ k) = A |^ m by B, FLANG_1:34;
    then consider a, b such that
B1:   a in A |^ n & b in A |^ k & x = a ^ b by A1, FLANG_1:def 1;
    a = x by B1, A, TARSKI:def 1;
    then b = <%>E by B1, LmSeq20;
    then <%>E in A by B, B1, FLANG_1:32;
    then <%>E in A |^ m & <%>E in A |^ n by FLANG_1:31;
    hence thesis by A, TARSKI:def 1;
  end;
  suppose m < n;
    then consider k such that
B:    m + k = n & k > 0 by LmNum30;
    (A |^ m) ^^ (A |^ k) = A |^ n by B, FLANG_1:34;
    then consider a, b such that
B1:   a in A |^ m & b in A |^ k & x = a ^ b by A1, FLANG_1:def 1;
    a = x by B1, A, TARSKI:def 1;
    then b = <%>E by B1, LmSeq20;
    then <%>E in A by B, B1, FLANG_1:32;
    then <%>E in A |^ m & <%>E in A |^ n by FLANG_1:31;
    hence thesis by A, TARSKI:def 1;
  end;
end;

theorem 
(A |^ m) |^ n = (A |^ n) |^ m
proof
  thus (A |^ m) |^ n = A |^ (m * n) by FLANG_1:35
                    .= (A |^ n) |^ m by FLANG_1:35;
end;

theorem LmLang50:
(A |^ m) ^^ (A |^ n) = (A |^ n) ^^ (A |^ m)
proof
  thus (A |^ m) ^^ (A |^ n) = A |^ (m + n) by FLANG_1:34
                           .= (A |^ n) ^^ (A |^ m)  by FLANG_1:34;
end;

theorem
<%>E in B implies A c= A ^^ (B |^ l) & A c= (B |^ l) ^^ A
proof
  assume <%>E in B;
  then <%>E in B |^ l by FLANG_1:31;
  hence thesis by FLANG_1:17;
end;  

theorem
A c= C |^ k & B c= C |^ l implies A ^^ B c= C |^ (k + l)
proof
  assume A c= C |^ k & B c= C |^ l;
  then A ^^ B c= (C |^ k) ^^ (C |^ l) by FLANG_1:18;
  hence thesis by FLANG_1:34;
end;

theorem 
x in A & x <> <%>E implies A* <> {<%>E}
proof
  assume x in A & x <> <%>E;
  then A <> {} & A <> {<%>E} by TARSKI:def 1;
  hence thesis by FLANG_1:48;
end;

theorem LmLang70:
<%>E in A & n > 0 implies (A |^ n)* = A*
proof
  assume 
A:  <%>E in A & n > 0;
B: 
  A* c= (A |^ n)*
  proof
    A c= A |^ n by A, FLANG_1:36;
    hence thesis by FLANG_1:62;
  end;
  (A |^ n)* c= A* by FLANG_1:65;
  hence thesis by B, XBOOLE_0:def 10;
end;

theorem LmLang80:
<%>E in A implies (A |^ n)* = (A*) |^ n
proof
  assume 
A:  <%>E in A;
  per cases;
  suppose 
B:  n = 0;
    thus (A |^ n)* = {<%>E}* by FLANG_1:25, B
                  .= {<%>E} by FLANG_1:48
                  .= (A*) |^ n by B, FLANG_1:25;
  end;
  suppose 
C:  n > 0;
    then (A*) |^ n = A* by FLANG_1:67;
    hence thesis by A, C, LmLang70;
  end;
end;

theorem
A c= A ^^ (B*) & A c= (B*) ^^ A
proof
  <%>E in B* by FLANG_1:49;
  hence thesis by FLANG_1:17;
end;

begin

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Union of a Range of Powers
:: Definition of |^ (n, m)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

definition
  let E, A;
  let m, n;
  func A |^ (m, n) -> Subset of E^omega equals 
    union { B: ex k st m <= k & k <= n & B = A |^ k };
  coherence
  proof                                            
    defpred P[set] means ex k st m <= k & k <= n & $1 = A |^ k;
    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;

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Union of a Range of Powers
:: Properties of |^ (n, m)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

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

theorem ThRange20:
m <= k & k <= n implies A |^ k c= A |^ (m, n)
proof
  assume m <= k & k <= n;
  then for x holds x in A |^ k implies x in A |^ (m, n) by ThRange10;
  hence thesis by TARSKI:def 3;    
end;

theorem ThRange30:
A |^ (m, n) = {} iff m > n or (m > 0 & A = {})
proof
  thus A |^ (m, n) = {} implies m > n or (m > 0 & A = {})
  proof
    assume that 
A1:   A |^ (m, n) = {} and
A2:   m <= n & (m <= 0 or A <> {});
B:  now 
      assume 
B1:     m <= n & m = 0;
      then {<%>E} = A |^ m by FLANG_1:30;
      then <%>E in A |^ m by TARSKI:def 1;
      hence contradiction by A1, B1, ThRange10;
    end;
    now 
      assume 
C1:     m <= n & A <> {};
      then A |^ m <> {} by FLANG_1:28;
      then ex a st a in A |^ m by SUBSET_1:10;      
      hence contradiction by A1, C1, ThRange10;
    end;
    hence thesis by A2, B;      
  end;
A:  
  now
    assume 
A1:   m > n;
    now
      let x;
      not (ex k st m <= k & k <= n & x in A |^ k) by A1, XXREAL_0:2;
      hence not x in A |^ (m, n) by ThRange10;
    end;  
    hence A |^ (m, n) = {} by XBOOLE_0:def 1;
  end;  
  now 
    assume 
B:    m > 0 & A = {};
    now
      let x;
      assume x in A |^ (m, n);
      then consider k such that
B1:      m <= k & k <= n & x in A |^ k by ThRange10;
      thus contradiction by B, B1, FLANG_1:28;
    end;  
    hence A |^ (m, n) = {} by XBOOLE_0:def 1;
  end;
  hence thesis by A;  
end;

theorem ThRange40: 
A |^ (m, m) = A |^ m
proof
A:
  now
    let x;
    assume x in A |^ (m, m);
    then consider k such that
A1:   m <= k & k <= m & x in A |^ k by ThRange10;
    thus x in A |^ m by A1, XXREAL_0:1;
  end;
  for x holds x in A |^ m implies x in A |^ (m, m) by ThRange10;  
  hence thesis by A, TARSKI:2;
end;

theorem ThRange50:
m <= k & l <= n implies A |^ (k, l) c= A |^ (m, n)
proof
  assume
A:  m <= k & l <= n;
  thus thesis
  proof
    let x;
    assume x in A |^ (k, l);
    then consider kl such that
B:    k <= kl & kl <= l & x in A |^ kl by ThRange10;
    m <= kl & kl <= n by A, B, XXREAL_0:2;
    hence x in A |^ (m, n) by B, ThRange10;
  end;
end;

theorem 
m <= k & k <= n implies A |^ (m, n) = A |^ (m, k) \/ A |^ (k, n)
proof
  assume 
A:  m <= k & k <= n;
B:  
  A |^ (m, n) c= A |^ (m, k) \/ A |^ (k, n)
  proof
    let x;
    assume x in A |^ (m, n);
    then consider l such that
B1:   m <= l & l <= n & x in A |^ l by ThRange10;
    l <= k or l > k;
    then x in A |^ (m, k) or x in A |^ (k, n) by B1, ThRange10;
    hence x in A |^ (m, k) \/ A |^ (k, n) by XBOOLE_0:def 2; 
  end;
  A |^ (m, k) \/ A |^ (k, n) c= A |^ (m, n)
  proof
    A |^ (m, k) c= A |^ (m, n) & A |^ (k, n) c= A |^ (m, n) by A, ThRange50;
    hence thesis by XBOOLE_1:8;
  end;
  hence thesis by B, XBOOLE_0:def 10;
end;

theorem ThRange70:
m <= k & k <= n implies A |^ (m, n) = A |^ (m, k) \/ A |^ (k + 1, n) 
proof
  assume 
A:  m <= k & k <= n;
  per cases;
  suppose k < n;
    then m <= k & m <= k + 1 & k <= n & k + 1 <= n by A, NAT_1:13;
    then A |^ (m, k) c= A |^ (m, n) &
         A |^ (k + 1, n) c= A |^ (m, n) by ThRange50;
    then
B:    A |^ (m, k) \/ A |^ (k + 1, n) c= A |^ (m, n) by XBOOLE_1:8;
    A |^ (m, n) c= A |^ (m, k) \/ A |^ (k + 1, n)
    proof
      let x;
      assume x in A |^ (m, n);
      then consider mn such that
C:      m <= mn & mn <= n & x in A |^ mn by ThRange10;
D:    mn <= k implies x in A |^ (m, k) by C, ThRange10;
      mn >= k + 1 implies x in A |^ (k + 1, n) by C, ThRange10;
      hence x in A |^ (m, k) \/ A |^ (k + 1, n) by D, NAT_1:13, XBOOLE_0:def 2;
    end;
    hence thesis by B, XBOOLE_0:def 10;
  end;
  suppose 
B:  k >= n;
    then k + 1 > n + 0 by XREAL_1:10;
    then A |^ (k + 1, n) = {} by ThRange30;
    hence thesis by B, A, XXREAL_0:1;
  end;  
end;

theorem ThRange80:
m <= n + 1 implies A |^ (m, n + 1) = A |^ (m, n) \/ (A |^ (n + 1))
proof
  assume 
A:  m <= n + 1;
  per cases by A, NAT_1:8;
  suppose m <= n;
    then m <= n & n < n + 1 by NAT_1:13;
    then A |^ (m, n + 1) = A |^ (m, n) \/ A |^ (n + 1, n + 1) by ThRange70;
    hence thesis by ThRange40;
  end;
  suppose 
B:  m = n + 1;
    then 
C:    m > n by NAT_1:13;
    thus A |^ (m, n + 1) = {} \/ A |^ (n + 1) by B, ThRange40
                        .= A |^ (m, n) \/ A |^ (n + 1) by C, ThRange30;  
  end;
end;

theorem 
m <= n implies A |^ (m, n) = A |^ m \/ A |^ (m + 1, n)
proof
  assume 
A:  m <= n;
  per cases by A, REAL_1:def 5;
  suppose m < n;
    then A |^ (m, n) = A |^ (m, m) \/ A |^ (m + 1, n) by ThRange70;
    hence thesis by ThRange40;
  end;
  suppose 
B:  m = n;
    then
C:    m + 1 > n by NAT_1:13;    
    thus A |^ (m, n) = A |^ m \/ {} by B, ThRange40
                    .= A |^ m \/ A |^ (m + 1, n) by C, ThRange30;  
  end;
end;

theorem ThRange100:
A |^ (n, n + 1) = A |^ n \/ A |^ (n + 1)
proof
  n <= n + 1 by NAT_1:11;
  hence A |^ (n, n + 1) = A |^ (n, n) \/ A |^ (n + 1) by ThRange80
                       .= A |^ n \/ A |^ (n + 1) by ThRange40; 
end;

theorem ThRange110:
A c= B implies A |^ (m, n) c= B |^ (m, n)
proof
  assume 
A:  A c= B;
  thus thesis
  proof
    let x;
    assume x in A |^ (m, n);
    then consider k such that
B:     m <= k & k <= n & x in A |^ k by ThRange10;
    A |^ k c= B |^ k by A, FLANG_1:38;
    hence x in B |^ (m, n) by B, ThRange10;  
  end;
end;

theorem ThRange120:
x in A & x <> <%>E & (m > 0 or n > 0) implies A |^ (m, n) <> {<%>E}
proof
  assume that 
A1: x in A & x <> <%>E and
A2: (m > 0 or n > 0);
  per cases by A2;
  suppose m > n;
    hence thesis by ThRange30;
  end;
  suppose 
B:  m <= n & m > 0;
    then 
B1:   A |^ m <> {<%>E} by A1, LmLang20;
    A |^ m <> {} by A1, FLANG_1:28;
    then consider x such that
B2:   x in A |^ m & x <> <%>E by B1, ZFMISC_1:41;
    A |^ m c= A |^ (m, n) by B, ThRange20;
    hence thesis by B2, TARSKI:def 1;   
  end;
  suppose 
B:  m <= n & n > 0;
    then 
B1:   A |^ n <> {<%>E} by A1, LmLang20;
    A |^ n <> {} by A1, FLANG_1:28;
    then consider x such that
B2:   x in A |^ n & x <> <%>E by B1, ZFMISC_1:41;
    A |^ n c= A |^ (m, n) by B, ThRange20;
    hence thesis by B2, TARSKI:def 1;   
  end;
end;

theorem ThRange130:
A |^ (m, n) = {<%>E} iff 
  (m <= n & A = {<%>E}) or (m = 0 & n = 0) or (m = 0 & A = {})
proof
  thus A |^ (m, n) = {<%>E} implies 
    (m <= n & A = {<%>E}) or (m = 0 & n = 0) or (m = 0 & A = {})
  proof
    assume that 
A:    A |^ (m, n) = {<%>E} and
B:    (m > n or A <> {<%>E}) & (m <> 0 or n <> 0) & (m <> 0 or A <> {});
    per cases by B;
    suppose m > n;
      hence contradiction by A, ThRange30;
    end;
    suppose 
B1:   m <= n & A <> {<%>E} & (m <> 0 or (n <> 0 & A <> {}));
      per cases by B1;
      suppose 
B1a:    m <> 0;
        per cases;
        suppose 
B1b:      A = {};
          m > 0 by B1a;  
          hence contradiction by A, B1b, ThRange30;
        end;
        suppose A <> {};
          then consider x such that 
B1c:      x in A & x <> <%>E by B1, ZFMISC_1:41;
          m > 0 by B1a;  
          hence contradiction by A, B1c, ThRange120;
        end;
      end;
      suppose 
B1a:    n <> 0 & A <> {};
        then consider x such that 
B1b:      x in A & x <> <%>E by B1, ZFMISC_1:41;
        n > 0 by B1a;  
        hence contradiction by A, B1b, ThRange120;
      end;
    end; 
  end;
  assume 
C1: (m <= n & A = {<%>E}) or (m = 0 & n = 0) or (m = 0 & A = {});
  per cases by C1;
  suppose 
C2: m <= n & A = {<%>E};
C3: now
      let x;
      assume x in A |^ (m, n);
      then consider k such that
C3a:    m <= k & k <= n & x in {<%>E} |^ k by C2, ThRange10;
      thus x in {<%>E} by C3a, FLANG_1:30;
    end;
    now
      let x;
      assume x in {<%>E};
      then 
C4:     x in {<%>E} |^ m by FLANG_1:30;
      {<%>E} |^ m c= {<%>E} |^ (m, n) by C2, ThRange20;
      hence x in A |^ (m, n) by C4, C2;
    end; 
    hence thesis by C3, TARSKI:2;
  end;
  suppose 
D:  m = 0 & n = 0;
    A |^ (0, 0) = A |^ 0 by ThRange40
               .= {<%>E} by FLANG_1:30;
    hence thesis by D;
  end;  
  suppose 
E:  m = 0 & A = {};
E2: A |^ (1, n) = {}
    proof
      now
        let x;
        assume x in A |^ (1, n);
        then consider k such that
E3:       1 <= k & k <= n & x in A |^ k by ThRange10;
        thus contradiction by E, E3, FLANG_1:28;
      end;
      hence thesis by XBOOLE_0:def 1;
    end;
    A |^ (0, n) = A |^ (0, 0) \/ A |^ (0 + 1, n) by ThRange70
               .= A |^ 0 \/ A |^ (0 + 1, n) by ThRange40
               .= {<%>E} by E2, FLANG_1:30;
    hence thesis by E;            
  end;
end;

theorem ThRange140:
A |^ (m, n) c= A*
proof
  let x;
  assume x in A |^ (m, n);
  then consider k such that
A:  m <= k & k <= n & x in A |^ k by ThRange10;
  thus x in A* by A, FLANG_1:42;
end;

theorem ThRange150:
<%>E in A |^ (m, n) iff m = 0 or (m <= n & <%>E in A) 
proof
  thus <%>E in A |^ (m, n) implies m = 0 or (m <= n & <%>E in A) 
  proof
    assume that
A:  <%>E in A |^ (m, n) and
B:  m <> 0 & (m > n or not <%>E in A);
    per cases by B;
    suppose m <> 0 & m > n;
      hence contradiction by A, ThRange30;
    end;
    suppose 
B1:   m <> 0 & not <%>E in A; 
      consider k such that
B2:     m <= k & k <= n & <%>E in A |^ k by A, ThRange10;
      k > 0 by B1, B2;   
      hence contradiction by B1, B2, FLANG_1:32;
    end;
  end;
  assume
C:  m = 0 or (m <= n & <%>E in A);
  per cases by C;
  suppose 
C1: m = 0;
    {<%>E} = A |^ 0 by FLANG_1:30;
    then {<%>E} c= A |^ (0, n) & <%>E in {<%>E} by ThRange20, TARSKI:def 1;
    hence <%>E in A |^ (m, n) by C1;
  end;
  suppose 
C2: m <= n & <%>E in A;
    then 
C3: <%>E in A |^ m by FLANG_1:31;
    A |^ m c= A |^ (m, n) by C2, ThRange20;
    hence <%>E in A |^ (m, n) by C3;
  end;
end; 

theorem ThRange160: 
<%>E in A & m <= n implies A |^ (m, n) = A |^ n
proof
  assume
A:  <%>E in A & m <= n;
B:
  A |^ (m, n) c= A |^ n
  proof
C0:  
    now
      let k such that 
C:      k <= n;
      per cases by C, REAL_1:def 5;
      suppose k < n;
        hence A |^ k c= A |^ n by A, FLANG_1:37;
      end;
      suppose k = n;
        hence A |^ k c= A |^ n;
      end;
    end;    
    let x such that
D:    x in A |^ (m, n);
    consider k such that
E:    m <= k & k <= n & x in A |^ k by D, ThRange10;
    A |^ k c= A |^ n by E, C0;
    hence x in A |^ n by E;
  end;
  A |^ n c= A |^ (m, n) by A, ThRange20;
  hence thesis by B, XBOOLE_0:def 10;   
end;

theorem ThRange240:
A |^ (m, n) ^^ (A |^ k) = (A |^ k) ^^ (A |^ (m, n))
proof
A:
  now
    let x;
    assume x in (A |^ (m, n)) ^^ (A |^ k);
    then consider a, b such that
A1:   a in A |^ (m, n) & b in (A |^ k) & x = a ^ b by FLANG_1:def 1;
    consider mn such that
A2:   m <= mn & mn <= n & a in A |^ mn by A1, ThRange10;
    a ^ b in (A |^ mn) ^^ (A |^ k) by A1, A2, FLANG_1:def 1;
    then 
A3:   a ^ b in (A |^ k) ^^ (A |^ mn) by LmLang50;
    A |^ mn c= A |^ (m, n) by A2, ThRange20;
    then (A |^ k) ^^ (A |^ mn) c= (A |^ k) ^^ (A |^ (m, n)) by FLANG_1:18;
    hence x in (A |^ k) ^^ (A |^ (m, n)) by A3, A1;
  end;
  now
    let x;
    assume x in (A |^ k) ^^ (A |^ (m, n));
    then consider a, b such that
A1:   a in (A |^ k) & b in A |^ (m, n) & x = a ^ b by FLANG_1:def 1;
    consider mn such that
A2:   m <= mn & mn <= n & b in A |^ mn by A1, ThRange10;
    a ^ b in (A |^ k) ^^ (A |^ mn) by A1, A2, FLANG_1:def 1;
    then 
A3:   a ^ b in (A |^ mn) ^^ (A |^ k) by LmLang50;
    A |^ mn c= A |^ (m, n) by A2, ThRange20;
    then (A |^ mn) ^^ (A |^ k) c= (A |^ (m, n)) ^^ (A |^ k) by FLANG_1:18;
    hence x in (A |^ (m, n)) ^^ (A |^ k) by A3, A1;
  end;
  hence thesis by A, TARSKI:2;
end;

theorem ThRange170:
(A |^ (m, n)) ^^ A = A ^^ (A |^ (m, n))
proof
  thus (A |^ (m, n)) ^^ A = (A |^ (m, n)) ^^ (A |^ 1) by FLANG_1:26
                         .= (A |^ 1) ^^ (A |^ (m, n)) by ThRange240
                         .= A ^^ (A |^ (m, n)) by FLANG_1:26;
end;

theorem ThRange190:
m <= n & k <= l implies (A |^ (m, n)) ^^ (A |^ (k, l)) = A |^ (m + k, n + l)
proof
  assume
A0: m <= n & k <= l;  
A:  
  now
    let x;
    assume x in (A |^ (m, n)) ^^ (A |^ (k, l));
    then consider a, b such that
A1:   a in A |^ (m, n) & b in A |^ (k, l) & x = a ^ b by FLANG_1:def 1;
    consider mn such that
A2:   m <= mn & mn <= n & a in A |^ mn by A1, ThRange10;
    consider kl such that
A3:   k <= kl & kl <= l & b in A |^ kl by A1, ThRange10;
A4: a ^ b in A |^ (mn + kl) by A2, A3, FLANG_1:41;
A5: m + k <= mn + kl by A2, A3, XREAL_1:9;
    mn + kl <= n + l by A2, A3, XREAL_1:9;
    hence x in A |^ (m + k, n + l) by A1, A4, A5, ThRange10;
  end;
  now
    let x;
    assume x in A |^ (m + k, n + l);
    then consider i such that
A1:   m + k <= i & i <= n + l & x in A |^ i by ThRange10;
    consider mn, kl such that
A2:   mn + kl = i & m <= mn & mn <= n & k <= kl & kl <= l by A0, A1, LmNum20;
A3: A |^ mn c= A |^ (m, n) by A2, ThRange20;
    A |^ kl c= A |^ (k, l) by A2, ThRange20;
    then (A |^ mn) ^^ (A |^ kl) c= 
           (A |^ (m, n)) ^^ (A |^ (k, l)) by A3, FLANG_1:18;
    then (A |^ (mn + kl)) c= (A |^ (m, n)) ^^ (A |^ (k, l)) by FLANG_1:34;
    hence x in (A |^ (m, n)) ^^ (A |^ (k, l)) by A1, A2; 
  end;
  hence thesis by A, TARSKI:2;
end;

theorem ThRange180:
A |^ (m + 1, n + 1) = (A |^ (m, n)) ^^ A
proof
  per cases;
  suppose m <= n;
    hence A |^ (m + 1, n + 1) = (A |^ (m, n)) ^^ (A |^ (1, 1)) by ThRange190
                            .= (A |^ (m, n)) ^^ (A |^ 1) by ThRange40
                            .= (A |^ (m, n)) ^^ A by FLANG_1:26;
  end;
  suppose 
A:  m > n;
    then A |^ (m, n) = {} by ThRange30;
    then 
A1:   (A |^ (m, n)) ^^ A = {} by FLANG_1:13;
    m + 1 > n + 1 by A, XREAL_1:10;
    hence A |^ (m + 1, n + 1) = (A |^ (m, n)) ^^ A by A1, ThRange30;
  end;                          
end;

theorem ThRange200:
(A |^ (m, n)) ^^ (A |^ (k, l)) = (A |^ (k, l)) ^^ (A |^ (m, n))
proof
  per cases;
  suppose 
A:  m <= n & k <= l;
    thus (A |^ (m, n)) ^^ (A |^ (k, l)) 
           = A |^ (m + k, n + l) by A, ThRange190
          .= (A |^ (k, l)) ^^ (A |^ (m, n)) by A, ThRange190;
  end;
  suppose m > n;
    then A |^ (m, n) = {} by ThRange30;
    then (A |^ (m, n)) ^^ (A |^ (k, l)) = {} &
         (A |^ (k, l)) ^^ (A |^ (m, n)) = {} by FLANG_1:13;
    hence thesis;
  end;          
  suppose k > l;
    then A |^ (k, l) = {} by ThRange30;
    then (A |^ (m, n)) ^^ (A |^ (k, l)) = {} &
         (A |^ (k, l)) ^^ (A |^ (m, n)) = {} by FLANG_1:13;
    hence thesis;
  end;          
end;

theorem ThRange210:
(A |^ (m, n)) |^ k = A |^ (m * k, n * k)
proof
  per cases;
  suppose 
Aa: m <= n;
    defpred P[Nat] means (A |^ (m, n)) |^ $1 = A |^ (m * $1, n * $1);
A:  P[0]
    proof
      thus (A |^ (m, n)) |^ 0 = {<%>E} by FLANG_1:25
                             .= A |^ 0 by FLANG_1:25
                             .= A |^ (m * 0, n * 0) by ThRange40; 
    end;
B:  now
      let k;
Ab:   m * k <= n * k by Aa, XREAL_1:66;
      assume 
B1:     P[k];
      (A |^ (m, n)) |^ (k + 1) 
        = (A |^ (m * k, n * k)) ^^ (A |^ (m, n)) by B1, FLANG_1:24
       .= A |^ (m * k + m, n * k + n) by Aa, Ab, ThRange190
       .= A |^ (m * (k + 1), n * (k + 1));
      hence P[k + 1];
    end;
    for k holds P[k] from NAT_1:sch 2(A, B);
    hence thesis;
  end;
  suppose 
C:  k = 0;
    hence (A |^ (m, n)) |^ k = {<%>E} by FLANG_1:25
                            .= A |^ 0  by FLANG_1:25
                            .= A |^ (m * k, n * k) by C, ThRange40;
  end;  
  suppose 
D:  m > n & k <> 0;
D1: k > 0 by D;
    A |^ (m, n) = {} by D, ThRange30;
    then 
D2:   (A |^ (m, n)) |^ k = {} by D1, FLANG_1:28;
    m * k > n * k by D, D1, XREAL_1:70;
    hence thesis by D2, ThRange30;
  end;  
end;

theorem ThRange211:
(A |^ (k + 1)) |^ (m, n) c= ((A |^ k) |^ (m, n)) ^^ (A |^ (m, n)) 
proof
  let x;
  assume x in (A |^ (k + 1)) |^ (m, n);
  then consider mn such that
A2: m <= mn & mn <= n & x in (A |^ (k + 1)) |^ mn by ThRange10;
  x in A |^ ((k + 1) * mn) by A2, FLANG_1:35;
  then x in A |^ (k * mn + mn);
  then x in (A |^ (k * mn)) ^^ (A |^ mn) by FLANG_1:34;
  then 
A4: x in ((A |^ k) |^ mn) ^^ (A |^ mn) by FLANG_1:35;
  (A |^ k) |^ mn c= (A |^ k) |^ (m, n) by A2, ThRange20;
  then ((A |^ k) |^ mn) ^^ (A |^ mn) c= 
    ((A |^ k) |^ (m, n)) ^^ (A |^ mn) by FLANG_1:18;
  then 
A5: x in ((A |^ k) |^ (m, n)) ^^ (A |^ mn) by A4;
  A |^ mn c= A |^ (m, n) by A2, ThRange20;
  then ((A |^ k) |^ (m, n)) ^^ (A |^ mn) c=
    ((A |^ k) |^ (m, n)) ^^ (A |^ (m, n)) by FLANG_1:18;
  hence x in ((A |^ k) |^ (m, n)) ^^ (A |^ (m, n)) by A5; 
end;

theorem ThRange220:
(A |^ k) |^ (m, n) c= A |^ (k * m, k * n)
proof
  per cases;
  suppose 
A:  m <= n;
    defpred P[Nat] means (A |^ $1) |^ (m, n) c= A |^ ($1 * m, $1 * n);
B:  P[0]
    proof
      (A |^ 0) |^ (m, n) = {<%>E} |^ (m, n) by FLANG_1:25
                        .= {<%>E} by A, ThRange130
                        .= A |^ 0 by FLANG_1:25
                        .= A |^ (0 * m, 0 * n) by ThRange40;
      hence thesis;                   
    end;
C:  now
      let l;
C0:   l * m <= l * n by A, XREAL_1:66;      
      assume 
C1:     P[l];
      (A |^ (l + 1)) |^ (m, n) 
        c= ((A |^ l) |^ (m, n)) ^^ (A |^ (m, n)) by ThRange211;
      then
C2:     (A |^ (l + 1)) |^ (m, n) 
          c= ((A |^ l) |^ (m, n)) ^^ ((A |^ 1) |^ (m, n)) by FLANG_1:26;   
C3:   ((A |^ l) |^ (m, n)) ^^ ((A |^ 1) |^ (m, n))  
        c= (A |^ (l * m, l * n)) ^^ ((A |^ 1) |^ (m, n)) by C1, FLANG_1:18;
      (A |^ (l * m, l * n)) ^^ ((A |^ 1) |^ (m, n))
        = (A |^ (l * m, l * n)) ^^ (A |^ (m, n)) by FLANG_1:26
       .= A |^ (l * m + m, l * n + n) by A, C0, ThRange190
       .= A |^ ((l + 1) * m, (l + 1) * n);
      hence P[l + 1] by C2, C3, XBOOLE_1:1;
    end;
    for l holds P[l] from NAT_1:sch 2(B, C);
    hence thesis;
  end;
  suppose m > n;
    then (A |^ k) |^ (m, n) = {} by ThRange30;
    hence thesis by XBOOLE_1:2;
  end;  
end;

theorem 
(A |^ k) |^ (m, n) c= (A |^ (m, n)) |^ k
proof
  (A |^ (m, n)) |^ k = A |^ (m * k, n * k) by ThRange210;
  hence thesis by ThRange220;
end;

theorem 
(A |^ (k + l)) |^ (m, n) c= ((A |^ k) |^ (m, n)) ^^ ((A |^ l) |^ (m, n)) 
proof
  let x;
  assume x in (A |^ (k + l)) |^ (m, n);
  then consider mn such that
A:  m <= mn & mn <= n & x in (A |^ (k + l)) |^ mn by ThRange10;
  x in A |^ ((k + l) * mn) by A, FLANG_1:35;
  then x in A |^ (k * mn + l * mn);
  then x in (A |^ (k * mn)) ^^ (A |^ (l * mn)) by FLANG_1:34;
  then consider a, b such that
B:  a in A |^ (k * mn) & b in A |^ (l * mn) & x = a ^ b by FLANG_1:def 1;
  a in (A |^ k) |^ mn & b in (A |^ l) |^ mn by B, FLANG_1:35;
  then a in (A |^ k) |^ (m, n) & b in (A |^ l) |^ (m, n) by A, ThRange10;
  hence x in (A |^ k) |^ (m, n) ^^ (A |^ l) |^ (m, n) by B, FLANG_1:def 1;
end;

theorem ThRange250:
A |^ (0, 0) = {<%>E}
proof
  thus A |^ (0, 0) = A |^ 0 by ThRange40
                  .= {<%>E} by FLANG_1:25;
end;

theorem ThRange260:
A |^ (0, 1) = {<%>E} \/ A
proof
  thus A |^ (0, 1) = A |^ 0 \/ A |^ (0 + 1) by ThRange100
                  .= {<%>E} \/ A |^ 1 by FLANG_1:25
                  .= {<%>E} \/ A by FLANG_1:26;
end;

theorem 
A |^ (1, 1) = A
proof
  thus A |^ (1, 1) = A |^ 1 by ThRange40
                  .= A by FLANG_1:26;
end;

theorem 
A |^ (0, 2) = {<%>E} \/ A \/ (A ^^ A)
proof
  thus A |^ (0, 2) = A |^ (0, 1) \/ A |^ (1 + 1) by ThRange80
                  .= {<%>E} \/ A \/ A |^ (1 + 1) by ThRange260
                  .= {<%>E} \/ A \/ (A ^^ A) by FLANG_1:27;
end;

theorem 
A |^ (1, 2) = A \/ (A ^^ A)
proof         
  thus A |^ (1, 2) = A |^ 1 \/ A |^ (1 + 1) by ThRange100
                  .= A \/ A |^ 2 by FLANG_1:26
                  .= A \/ (A ^^ A) by FLANG_1:27;
end;                  

theorem 
A |^ (2, 2) = A ^^ A
proof
  thus A |^ (2, 2) = A |^ 2 by ThRange40
                  .= A ^^ A by FLANG_1:27;
end;

theorem ThRange302:
m > 0 & m <> n & A |^ (m, n) = {x} implies
  for mn st m <= mn & mn <= n holds A |^ mn = {x}
proof
  assume 
A1: m > 0 & m <> n & A |^ (m, n) = {x};
  given mn such that
A2: m <= mn & mn <= n & A |^ mn <> {x};
  per cases;
  suppose A |^ mn = {};
    then 
B1:   A = {} by FLANG_1:28;
    x in A |^ (m, n) by A1, TARSKI:def 1;
    then consider i such that 
B2:   m <= i & i <= n & x in A |^ i by ThRange10;
    thus contradiction by A1, B1, B2, FLANG_1:28; 
  end;
  suppose A |^ mn <> {};
    then consider y such that
B1:   y in A |^ mn & y <> x by A2, ZFMISC_1:41;
    y in A |^ (m, n) by B1, A2, ThRange10;   
    hence contradiction by TARSKI:def 1, A1, B1; 
  end;
end;   

theorem ThRange310:
m <> n & A |^ (m, n) = {x} implies x = <%>E
proof
  assume  
A:  m <> n & A |^ (m, n) = {x};
  per cases;
  suppose m > n;
    hence thesis by A, ThRange30;
  end;
  suppose 
B:  m = 0 & m <= n;
    then {<%>E} = A |^ m by FLANG_1:25;
    then <%>E in A |^ m by TARSKI:def 1;
    then <%>E in A |^ (m, n) by B, ThRange10;
    hence thesis by A, TARSKI:def 1;
  end;
  suppose m > 0 & m <= n;
    then A |^ m = {x} & A |^ n = {x} by A, ThRange302;
    hence thesis by A, LmLang32;
  end;
end;

theorem ThRange320:
<%x%> in A |^ (m, n) iff 
  <%x%> in A & m <= n & ((<%>E in A & (n > 0)) or (m <= 1 & 1 <= n))
proof
  thus <%x%> in A |^ (m, n) implies 
    <%x%> in A & m <= n & ((<%>E in A & (n > 0)) or (m <= 1 & 1 <= n))
  proof
    assume 
A:    <%x%> in A |^ (m, n);
    then consider mn such that
B:    m <= mn & mn <= n & <%x%> in A |^ mn by ThRange10;
    thus thesis by A, B, LmLang31, ThRange30;
  end;
  assume 
A:  <%x%> in A & m <= n & ((<%>E in A & (n > 0)) or (m <= 1 & 1 <= n));
  per cases by A;
  suppose <%>E in A & (n > 0);
    then A c= A |^ n by FLANG_1:36;
    hence thesis by A, ThRange10;
  end;
  suppose 
B:  m <= 1 & 1 <= n;
    <%x%> in A |^ 1 by A, FLANG_1:26;
    hence thesis by B, ThRange10; 
  end;
end;

theorem 
(A /\ B) |^ (m, n) c= (A |^ (m, n)) /\ (B |^ (m, n))
proof
  let x;
  assume x in (A /\ B) |^ (m, n);
  then consider mn such that
A:  m <= mn & mn <= n & x in (A /\ B) |^ mn by ThRange10;
  (A /\ B) |^ mn c= (A |^ mn) /\ (B |^ mn) by FLANG_1:40;
  then x in A |^ mn & x in B |^ mn by A, XBOOLE_0:def 3;
  then x in A |^ (m, n) & x in B |^ (m, n) by A, ThRange10;
  hence x in (A |^ (m, n)) /\ (B |^ (m, n)) by XBOOLE_0:def 3;
end;

theorem 
(A |^ (m, n)) \/ (B |^ (m, n)) c= (A \/ B) |^ (m, n)
proof
  let x;
  assume 
A:  x in (A |^ (m, n)) \/ (B |^ (m, n));
  per cases by A, XBOOLE_0:def 2;
  suppose x in A |^ (m, n);
    then consider mn such that
B:    m <= mn & mn <= n & x in A |^ mn by ThRange10;
C:  x in (A |^ mn) \/ (B |^ mn) by B, XBOOLE_0:def 2;
    (A |^ mn) \/ (B |^ mn) c= (A \/ B) |^ mn by FLANG_1:39;
    hence x in (A \/ B) |^ (m, n) by B, C, ThRange10;
  end;
  suppose x in B |^ (m, n);
    then consider mn such that
B:    m <= mn & mn <= n & x in B |^ mn by ThRange10;
C:  x in (A |^ mn) \/ (B |^ mn) by B, XBOOLE_0:def 2;
    (A |^ mn) \/ (B |^ mn) c= (A \/ B) |^ mn by FLANG_1:39;
    hence x in (A \/ B) |^ (m, n) by B, C, ThRange10;
  end;
end;

theorem 
(A |^ (m, n)) |^ (k, l) c= A |^ (m * k, n * l)
proof
  let x;
  assume x in (A |^ (m, n)) |^ (k, l);
  then consider kl such that
A1: k <= kl & kl <= l & x in (A |^ (m, n)) |^ kl by ThRange10;
A2: 
  x in A |^ (m * kl, n * kl) by A1, ThRange210;
  m * k <= m * kl & n * kl <= n * l by A1, NAT_1:4;
  then A |^ (m * kl, n * kl) c= A |^ (m * k, n * l) by ThRange50;
  hence x in A |^ (m * k, n * l) by A2;
end;

theorem
m <= n & <%>E in B implies A c= A ^^ (B |^ (m, n)) & A c= (B |^ (m, n)) ^^ A
proof
  assume m <= n & <%>E in B;
  then <%>E in B |^ (m, n) by ThRange150;
  hence thesis by FLANG_1:17;
end;  

theorem 
m <= n & k <= l & A c= C |^ (m, n) & B c= C |^ (k, l) implies 
  A ^^ B c= C |^ (m + k, n + l)
proof
  assume 
A:  m <= n & k <= l & A c= C |^ (m, n) & B c= C |^ (k, l);
  thus thesis
  proof
    let x;
    assume x in A ^^ B;
    then consider a, b such that
B:    a in A & b in B & x = a ^ b by FLANG_1:def 1;
    a ^ b in C |^ (m, n) ^^ C |^ (k, l) by FLANG_1:def 1, A, B;
    hence x in C |^ (m + k, n + l) by A, B, ThRange190;
  end;
end;  

theorem   
(A |^ (m, n))* c= A*
proof
  let x;
  assume x in (A |^ (m, n))*;
  then consider k such that
B:  x in A |^ (m, n) |^ k by FLANG_1:42; 
C:  
  A |^ (m, n) |^ k = A |^ (m * k, n * k) by ThRange210;
  A |^ (m * k, n * k) c= A* by ThRange140;
  hence x in A* by B, C;
end;  

theorem
(A*) |^ (m, n) c= A*
proof
  let x;
  assume x in (A*) |^ (m, n);
  then consider mn such that
A:  m <= mn & mn <= n & x in (A*) |^ mn by ThRange10;
  (A*) |^ mn c= A* by FLANG_1:66;
  hence x in A* by A;
end;  

theorem 
m <= n & n > 0 implies (A*) |^ (m, n) = A*
proof
  assume
A:  m <= n & n > 0;
  <%>E in A* by FLANG_1:49;
  hence (A*) |^ (m, n) = (A*) |^ n by A, ThRange160
                      .= A* by A, FLANG_1:67;   
end;  

theorem 
m <= n & n > 0 & <%>E in A implies (A |^ (m, n))* = A*
proof
  assume 
A:  m <= n & n > 0 & <%>E in A;
  thus (A |^ (m, n))* = (A |^ n)* by A, ThRange160
                     .= A* by A, LmLang70;
end;                

theorem
m <= n & <%>E in A implies (A |^ (m, n))* = (A*) |^ (m, n)
proof
  assume
A:  m <= n & <%>E in A;
  then 
B:  (A |^ (m, n))* = (A |^ n)* by ThRange160;
  <%>E in A* by FLANG_1:49;
  then A* |^ (m, n) = A* |^ n by A, ThRange160;
  hence thesis by A, B, LmLang80; 
end;  

theorem ThRange440:
A c= B* implies A |^ (m, n) c= B*
proof
  assume 
A:  A c= B*;
  thus thesis
  proof
    let x;
    assume x in A |^ (m, n);
    then consider mn such that
B:    m <= mn & mn <= n & x in A |^ mn by ThRange10;
    A |^ mn c= B* by A, FLANG_1:60;
    hence x in B* by B;  
  end;
end;  

theorem
A c= B* implies B* = (B \/ (A |^ (m, n)))*
proof
  assume A c= B*;
  then A |^ (m, n) c= B* by ThRange440;
  hence thesis by FLANG_1:68;
end;  

theorem ThRange450:
A |^ (m, n) ^^ (A*) = A* ^^ (A |^ (m, n))
proof
A0: 
  A |^ (m, n) ^^ (A*) c= A* ^^ (A |^ (m, n))
  proof
    let x;
    assume x in A |^ (m, n) ^^ (A*);
    then consider a, b such that
A1:   a in A |^ (m, n) & b in A* & x = a ^ b by FLANG_1:def 1;
    consider mn such that
A2:   m <= mn & mn <= n & a in A |^ mn by A1, ThRange10;
    consider k such that
A3:   b in A |^ k by A1, FLANG_1:42;
    a ^ b in A |^ (k + mn) by A2, A3, FLANG_1:41;
    then 
A4:   a ^ b in A |^ k ^^ (A |^ mn) by FLANG_1:34;
    A |^ k c= A* & A |^ mn c= A |^ (m, n) by FLANG_1:43, ThRange20, A2;
    then A |^ k ^^ (A |^ mn) c= A* ^^ (A |^ (m, n)) by FLANG_1:18;
    hence x in A* ^^ (A |^ (m, n)) by A1, A4;
  end;
  A* ^^ (A |^ (m, n)) c= A |^ (m, n) ^^ (A*)
  proof
    let x;
    assume x in A* ^^ (A |^ (m, n));
    then consider a, b such that
A1:   a in A* & b in A |^ (m, n) & x = a ^ b by FLANG_1:def 1;
    consider mn such that
A2:   m <= mn & mn <= n & b in A |^ mn by A1, ThRange10;
    consider k such that
A3:   a in A |^ k by A1, FLANG_1:42;
    a ^ b in A |^ (mn + k) by A2, A3, FLANG_1:41;
    then 
A4:   a ^ b in A |^ mn ^^ (A |^ k) by FLANG_1:34;
    A |^ k c= A* & A |^ mn c= A |^ (m, n) by FLANG_1:43, ThRange20, A2;
    then A |^ mn ^^ (A |^ k) c= A |^ (m, n) ^^ (A*) by FLANG_1:18;
    hence x in A |^ (m, n) ^^ (A*) by A1, A4;
  end;
  hence thesis by A0, XBOOLE_0:def 10;
end;  

theorem
<%>E in A & m <= n implies A* = A* ^^ (A |^ (m, n))
proof
  assume 
A:  <%>E in A & m <= n;
  defpred P[Nat] means A* = A* ^^ (A |^ (m, m + $1));
B1:  
  P[0]
  proof
    thus A* = A* ^^ (A |^ m) by A, FLANG_1:56
           .= A* ^^ (A |^ (m, m + 0)) by ThRange40;
  end;
B2:  
  now
    let i;
    assume 
B2a:  P[i];
    m <= m + (i + 1) by NAT_1:11;
    then A |^ (m, m + (i + 1)) 
      = A |^ (m, m + i) \/ (A |^ (m + i + 1)) by ThRange80;
    then A* ^^ (A |^ (m, m + (i + 1))) 
      = A* \/ (A* ^^ (A |^ (m + i + 1))) by B2a, FLANG_1:21
     .= A* \/ A* by A, FLANG_1:56;
    hence P[i + 1];
  end;
C:  
  for i holds P[i] from NAT_1:sch 2(B1, B2);
  consider k such that 
D:  m + k = n by A, NAT_1:10;
  thus thesis by C, D;  
end;  

theorem ThRange470:
A |^ (m, n) |^ k c= A*
proof
  let x;
  assume 
A:  x in A |^ (m, n) |^ k;
  A |^ (m, n) c= A* by ThRange140;
  then A |^ (m, n) |^ k c= A* by FLANG_1:60;
  hence x in A* by A;   
end;  

theorem ThRange480:
A |^ k |^ (m, n) c= A*
proof
  let x;
  assume x in A |^ k |^ (m, n);
  then consider mn such that
A:  m <= mn & mn <= n & x in A |^ k |^ mn by ThRange10;
B:  
  x in A |^ (k * mn) by A, FLANG_1:35;
  A |^ (k * mn) c= A* by FLANG_1:43;
  hence x in A* by B;   
end;  

theorem
m <= n implies (A |^ m)* c= (A |^ (m, n))*
proof
  assume m <= n;
  then A |^ m c= A |^ (m, n) by ThRange20;
  hence thesis by FLANG_1:62;
end;  

theorem ThRange500: 
(A |^ (m, n)) |^ (k, l) c= A*
proof
  let x;
  assume x in (A |^ (m, n)) |^ (k, l);
  then consider kl such that
A:  k <= kl & kl <= l & x in (A |^ (m, n)) |^ kl by ThRange10;
  (A |^ (m, n)) |^ kl c= A* by ThRange470;
  hence x in A* by A;
end;

theorem ThRange520:
<%>E in A & k <= n & l <= n implies A |^ (k, n) = A |^ (l, n)
proof
  assume 
A:  <%>E in A & k <= n & l <= n;
  hence A |^ (k, n) = A |^ n by ThRange160
                   .= A |^ (l, n) by A, ThRange160;
end;

begin

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Optional Occurrence
:: Definition of ?
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

definition
  let E, A;
  func A? -> Subset of E^omega equals  
    union { B: ex k st k <= 1 & B = A |^ k };
  coherence
  proof                                            
    defpred P[set] means ex k st k <= 1 & $1 = A |^ k;
    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;
  
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Optional Occurrence
:: Properties of ?
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

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

theorem 
n <= 1 implies A |^ n c= A?
proof
  assume n <= 1;
  then for x holds x in A |^ n implies x in A? by ThOpt10;
  hence thesis by TARSKI:def 3;    
end;

theorem ThOpt40:
A? = (A |^ 0) \/ (A |^ 1) 
proof
  now
    let x;
    x in A? iff ex k st (k = 0 or k = 1) & x in A |^ k
    proof
      thus x in A? implies ex k st (k = 0 or k = 1) & x in A |^ k
      proof
        assume x in A?;
        then consider k such that 
A:        k <= 1 & x in A |^ k by ThOpt10;
        (k = 0 or k = 1) by A, NAT_1:26;
        hence thesis by A;
      end;
      given k such that
B:      (k = 0 or k = 1) & x in A |^ k;
      thus thesis by B, ThOpt10;
    end;
    hence x in A? iff x in A |^ 0 or x in A |^ 1;
  end;  
  hence thesis by XBOOLE_0:def 2;  
end;

theorem ThOpt50:
A? = {<%>E} \/ A
proof
  A |^ 0 = {<%>E} & A |^ 1 = A by FLANG_1:25, FLANG_1:26; 
  hence thesis by ThOpt40;
end;

theorem 
A c= A?
proof
  A? = {<%>E} \/ A by ThOpt50;
  hence thesis by XBOOLE_1:7;
end;

theorem ThOpt60:
x in A? iff x = <%>E or x in A
proof
  x in A? iff x in {<%>E} \/ A by ThOpt50;
  then x in A? iff x in {<%>E} or x in A by XBOOLE_0:def 2;
  hence thesis by TARSKI:def 1;
end;

theorem ThOpt70:
A? = A |^ (0, 1)
proof
  thus A? = (A |^ 0) \/ (A |^ (0 + 1)) by ThOpt40
         .= A |^ (0, 1) by ThRange100;
end;

theorem ThOpt80:
A? = A iff <%>E in A
proof
  thus A? = A implies <%>E in A
  proof
    assume A? = A;
    then A = {<%>E} \/ A by ThOpt50;
    hence thesis by ZFMISC_1:45;
  end;
  assume <%>E in A;
  then A = {<%>E} \/ A by ZFMISC_1:46;
  hence thesis by ThOpt50;
end;

registration let E, A;
  cluster A? -> non empty;
  coherence
  proof
    <%>E in A? by ThOpt60;
    hence thesis;
  end;
end;

theorem
A?? = A?
proof
  <%>E in A? by ThOpt60;
  hence thesis by ThOpt80;
end;

theorem 
A c= B implies A? c= B?
proof
  assume A c= B;
  then A |^ (0, 1) c= B |^ (0, 1) by ThRange110;
  then A? c= B |^ (0, 1) by ThOpt70;
  hence thesis by ThOpt70;
end;

theorem 
x in A & x <> <%>E implies A? <> {<%>E}
proof
  assume
A:  x in A & x <> <%>E;
  A? = A |^ (0, 1) by ThOpt70;
  hence thesis by A, ThRange120;  
end;

theorem 
A? = {<%>E} iff A = {} or A = {<%>E}
proof
  A? = A |^ (0, 1) by ThOpt70;
  hence thesis by ThRange130;
end;

theorem 
(A*)? = A* & (A?)* = A*
proof
A:  
  <%>E in A* by FLANG_1:49;
  thus (A*)? = {<%>E} \/ (A*) by ThOpt50
            .= A* by A, ZFMISC_1:46;
  thus (A?)* = ({<%>E} \/ A)* by ThOpt50
            .= A* by A, FLANG_1:69;         
end;

theorem 
A? c= A*
proof
  A? = A |^ (0, 1) by ThOpt70;
  hence thesis by ThRange140;
end;

theorem
(A /\ B)? = (A?) /\ (B?)
proof
  thus (A /\ B)? = {<%>E} \/ (A /\ B) by ThOpt50
                .= ({<%>E} \/ A) /\ ({<%>E} \/ B) by XBOOLE_1:24
                .= (A?) /\ ({<%>E} \/ B) by ThOpt50
                .= (A?) /\ (B?) by ThOpt50;
end;

theorem
(A?) \/ (B?) = (A \/ B)?
proof
  thus (A \/ B)? = {<%>E} \/ (A \/ B) by ThOpt50
                .= (A \/ {<%>E}) \/ (B \/ {<%>E}) by XBOOLE_1:5
                .= (A?) \/ (B \/ {<%>E}) by ThOpt50
                .= (A?) \/ (B?) by ThOpt50;
end;

theorem
A? = {x} implies x = <%>E
proof
  A? = A |^ (0, 1) by ThOpt70;
  hence thesis by ThRange310;
end;

theorem
<%x%> in A? iff <%x%> in A
proof
  A? = A |^ (0, 1) by ThOpt70;
  hence thesis by ThRange320;
end;

theorem
(A?) ^^ A = A ^^ (A?)
proof
  A? = A |^ (0, 1) by ThOpt70;
  hence thesis by ThRange170;
end;

theorem
(A?) ^^ A = A |^ (1, 2)
proof
  A? = A |^ (0, 1) by ThOpt70;
  then (A?) ^^ A = A |^ (0 + 1, 1 + 1) by ThRange180;
  hence thesis;
end;

theorem ThOpt210:
(A?) ^^ (A?) = A |^ (0, 2)
proof
  A? = A |^ (0, 1) by ThOpt70;
  then (A?) ^^ (A?) = A |^ (0 + 0, 1 + 1) by ThRange190;
  hence thesis;
end;

theorem ThOpt220:
(A?) |^ k = (A?) |^ (0, k)
proof
  <%>E in A? by ThOpt60;
  hence thesis by ThRange160;
end;

theorem ThOpt230:
(A?) |^ k = A |^ (0, k)
proof
  defpred P[Nat] means (A?) |^ $1 = A |^ (0, $1);
A:  
  P[0]
  proof
    thus (A?) |^ 0 = {<%>E} by FLANG_1:25
                  .= A |^ (0, 0) by ThRange250;
  end;
B:  
  now
    let k;
    assume 
C:    P[k];
    (A?) |^ (k + 1) = ((A?) |^ k) ^^ ((A?) |^ 1) by FLANG_1:34
                   .= A |^ (0, k) ^^ (A?) by C, FLANG_1:26
                   .= A |^ (0, k) ^^ (A |^ (0, 1)) by ThOpt70
                   .= A |^ (0 + 0, k + 1) by ThRange190;
    hence P[k + 1];
  end;
  for k holds P[k] from NAT_1:sch 2(A, B);
  hence thesis;
end;

theorem ThOpt340:
m <= n implies A? |^ (m, n) = A? |^ (0, n)
proof
  assume
A:  m <= n;  
  <%>E in A? by ThOpt60;
  hence thesis by A, ThRange520;
end;  

theorem ThOpt350:
A? |^ (0, n) = A |^ (0, n)
proof
  thus A? |^ (0, n) = A? |^ n by ThOpt220
                   .= A |^ (0, n) by ThOpt230;
end;  

theorem ThOpt360:
m <= n implies A? |^ (m, n) = A |^ (0, n)
proof
  assume m <= n;
  hence A? |^ (m, n) = A? |^ (0, n) by ThOpt340
                    .= A |^ (0, n) by ThOpt350;
end;  

theorem
(A |^ (1, n))? = A |^ (0, n)
proof
  thus (A |^ (1, n))? = {<%>E} \/ (A |^ (1, n)) by ThOpt50
                     .= A |^ (0, 0) \/ (A |^ (0 + 1, n)) by ThRange250
                     .= A |^ (0, n) by ThRange70;
end;  

theorem 
<%>E in A & <%>E in B implies A? c= A ^^ B & A? c= B ^^ A
proof
  assume 
A:  <%>E in A & <%>E in B;
  then 
B:  A c= A ^^ B & A c= B ^^ A by FLANG_1:17;
  <%>E in A ^^ B & <%>E in B ^^ A by A, FLANG_1:16;
  then {<%>E} c= A ^^ B & {<%>E} c= B ^^ A by ZFMISC_1:37;
  then {<%>E} \/ A c= A ^^ B & {<%>E} \/ A c= B ^^ A by B, XBOOLE_1:8;
  hence thesis by ThOpt50;
end;  

theorem
A c= A ^^ (B?) & A c= (B?) ^^ A
proof
  <%>E in B? by ThOpt60;
  hence thesis by FLANG_1:17;
end;  

theorem
A c= C? & B c= C? implies A ^^ B c= C |^ (0, 2)
proof
  assume A c= C? & B c= C?;
  then A ^^ B c= (C?) ^^ (C?) by FLANG_1:18;
  hence thesis by ThOpt210;
end;  

theorem
<%>E in A & n > 0 implies A? c= A |^ n
proof
  assume <%>E in A & n > 0;
  then <%>E in A |^ n & A c= A |^ n by FLANG_1:31, FLANG_1:36;
  then {<%>E} c= A |^ n & A c= A |^ n by ZFMISC_1:37;
  then {<%>E} \/ A c= A |^ n by XBOOLE_1:8;
  hence thesis by ThOpt50;
end;  

theorem
(A?) ^^ (A |^ k) = (A |^ k) ^^ (A?)
proof
  thus (A?) ^^ (A |^ k) 
    = ({<%>E} \/ A) ^^ (A |^ k) by ThOpt50
   .= ({<%>E} ^^ (A |^ k)) \/ (A ^^ (A |^ k)) by FLANG_1:21
   .= ({<%>E} ^^ (A |^ k)) \/ ((A |^ k) ^^ A) by FLANG_1:33
   .= (A |^ k) \/ ((A |^ k) ^^ A) by FLANG_1:14
   .= ((A |^ k) ^^ {<%>E}) \/ ((A |^ k) ^^ A) by FLANG_1:14
   .= (A |^ k) ^^ (A \/ {<%>E}) by FLANG_1:21
   .= (A |^ k) ^^ (A?) by ThOpt50; 
end;
  
theorem ThOpt280:
A c= B* implies A? c= B*
proof
  assume A c= B*;
  then A |^ (0, 1) c= B* by ThRange440;
  hence thesis by ThOpt70;
end;  

theorem
A c= B* implies B* = (B \/ (A?))*
proof
  assume A c= B*;
  then A? c= B* by ThOpt280;
  hence thesis by FLANG_1:68;
end;  

theorem
A? ^^ (A*) = A* ^^ (A?)
proof
  thus A? ^^ (A*) = A |^ (0, 1) ^^ (A*) by ThOpt70
                 .= A* ^^ (A |^ (0, 1)) by ThRange450
                 .= A* ^^ (A?) by ThOpt70;
end;  

theorem
A? ^^ (A*) = A*
proof
A:
  A ^^ (A*) c= A* by FLANG_1:54;
  thus A? ^^ (A*) = ({<%>E} \/ A) ^^ (A*) by ThOpt50
                 .= {<%>E} ^^ (A*) \/ A ^^ (A*) by FLANG_1:21
                 .= A* \/ A ^^ (A*) by FLANG_1:14
                 .= A* by A, XBOOLE_1:12; 
end;  

theorem
A? |^ k c= A*
proof
  A? |^ k = (A |^ (0, 1)) |^ k by ThOpt70;
  hence thesis by ThRange470;
end;  

theorem
(A |^ k)? c= A*
proof
  (A |^ k)? = (A |^ k) |^ (0, 1) by ThOpt70;
  hence thesis by ThRange480;
end;  
 
theorem
(A?) ^^ (A |^ (m, n)) = (A |^ (m, n)) ^^ (A?)
proof
  (A |^ (0, 1)) ^^ (A |^ (m, n)) 
    = (A |^ (m, n)) ^^ (A |^ (0, 1)) by ThRange200;
  then (A?) ^^ (A |^ (m, n)) = (A |^ (m, n)) ^^ (A |^ (0, 1)) by ThOpt70;
  hence thesis by ThOpt70;  
end;

theorem
(A?) ^^ (A |^ k) = A |^ (k, k + 1)
proof
  (A |^ (0, 1)) ^^ (A |^ k) = (A |^ (0, 1)) ^^ (A |^ (k, k)) by ThRange40
                           .= A |^ (0 + k, 1 + k) by ThRange190;
  hence thesis by ThOpt70;                         
end;  

theorem
A? |^ (m, n) c= A*
proof
  per cases;
  suppose m <= n;
    then A? |^ (m, n) = A |^ (0, n) by ThOpt360;
    hence thesis by ThRange140;
  end;
  suppose m > n;
    then A? |^ (m, n) = {} by ThRange30;
    hence thesis by XBOOLE_1:2;
  end;    
end;  

theorem
(A |^ (m, n))? c= A*
proof
  (A |^ (m, n))? = (A |^ (m, n)) |^ (0, 1) by ThOpt70;
  hence thesis by ThRange500; 
end;  

theorem
A? = (A \ {<%>E})?
proof
  thus A? = {<%>E} \/ A by ThOpt50
         .= {<%>E} \/ (A \ {<%>E}) by XBOOLE_1:39
         .= (A \ {<%>E})? by ThOpt50;
end;  

theorem
A c= B? implies A? c= B?
proof
  assume 
A:  A c= B?;
  <%>E in B? by ThOpt60;
  then {<%>E} c= B? by ZFMISC_1:37;
  then {<%>E} \/ A c= B? by A, XBOOLE_1:8;
  hence thesis by ThOpt50;
end;  

theorem
A c= B? implies B? = (B \/ A)?
proof
  assume
A:  A c= B?;
  thus (B \/ A)? = {<%>E} \/ (B \/ A) by ThOpt50
                .= ({<%>E} \/ B) \/ A by XBOOLE_1:4
                .= B? \/ A by ThOpt50
                .= B? by A, XBOOLE_1:12; 
end;


Top