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


begin

:: Preliminaries - Numbers:
theorem Th1: :: FLANG_2:1
for m, k, i, n being Nat st m + k <= i &amp; i <= n + k holds
ex mn being Nat st
( mn + k = i &amp; m <= mn &amp; mn <= n )
proofend;

theorem Th2: :: FLANG_2:2
for m, n, k, l, i being Nat st m <= n &amp; k <= l &amp; m + k <= i &amp; i <= n + l holds
ex mn, kl being Nat st
( mn + kl = i &amp; m <= mn &amp; mn <= n &amp; k <= kl &amp; kl <= l )
proofend;

theorem Th3: :: FLANG_2:3
for m, n being Nat st m < n holds
ex k being Nat st
( m + k = n &amp; k > 0 )
proofend;

:: Preliminaries - Sequences:
theorem Th4: :: FLANG_2:4
for E being set
for a, b being Element of E ^omega st ( a ^ b = a or b ^ a = a ) holds
b = {}
proofend;

begin

:: Addenda - FLANG_1:
theorem :: FLANG_2:5
for x, E being set
for A, B being Subset of (E ^omega) st ( x in A or x in B ) &amp; x <> <%> E holds
A ^^ B <> {(<%> E)}
proofend;

theorem :: FLANG_2:6
for x, E being set
for A, B being Subset of (E ^omega) holds
( <%x%> in A ^^ B iff ( ( <%> E in A &amp; <%x%> in B ) or ( <%x%> in A &amp; <%> E in B ) ) )
proofend;

theorem Th7: :: FLANG_2:7
for x, E being set
for A being Subset of (E ^omega)
for n being Nat st x in A &amp; x <> <%> E &amp; n > 0 holds
A |^ n <> {(<%> E)}
proofend;

theorem :: FLANG_2:8
for E being set
for A being Subset of (E ^omega)
for n being Nat holds
( <%> E in A |^ n iff ( n = 0 or <%> E in A ) )
proofend;

theorem Th9: :: FLANG_2:9
for x, E being set
for A being Subset of (E ^omega)
for n being Nat holds
( <%x%> in A |^ n iff ( <%x%> in A &amp; ( ( <%> E in A &amp; n > 1 ) or n = 1 ) ) )
proofend;

theorem Th10: :: FLANG_2:10
for x, E being set
for A being Subset of (E ^omega)
for m, n being Nat st m <> n &amp; A |^ m = {x} &amp; A |^ n = {x} holds
x = <%> E
proofend;

theorem :: FLANG_2:11
for E being set
for A being Subset of (E ^omega)
for m, n being Nat holds (A |^ m) |^ n = (A |^ n) |^ m
proofend;

theorem Th12: :: FLANG_2:12
for E being set
for A being Subset of (E ^omega)
for m, n being Nat holds (A |^ m) ^^ (A |^ n) = (A |^ n) ^^ (A |^ m)
proofend;

theorem :: FLANG_2:13
for E being set
for B, A being Subset of (E ^omega)
for l being Nat st <%> E in B holds
( A c= A ^^ (B |^ l) &amp; A c= (B |^ l) ^^ A )
proofend;

theorem :: FLANG_2:14
for E being set
for A, C, B being Subset of (E ^omega)
for k, l being Nat st A c= C |^ k &amp; B c= C |^ l holds
A ^^ B c= C |^ (k + l)
proofend;

theorem :: FLANG_2:15
for x, E being set
for A being Subset of (E ^omega) st x in A &amp; x <> <%> E holds
A * <> {(<%> E)}
proofend;

theorem Th16: :: FLANG_2:16
for E being set
for A being Subset of (E ^omega)
for n being Nat st <%> E in A &amp; n > 0 holds
(A |^ n) * = A *
proofend;

theorem Th17: :: FLANG_2:17
for E being set
for A being Subset of (E ^omega)
for n being Nat st <%> E in A holds
(A |^ n) * = (A *) |^ n
proofend;

theorem :: FLANG_2:18
for E being set
for A, B being Subset of (E ^omega) holds
( A c= A ^^ (B *) &amp; A c= (B *) ^^ A )
proofend;

begin

:: Union of a Range of Powers
:: Definition of |^ (n, m)
definition
let E be set ;
let A be Subset of (E ^omega);
let m, n be Nat;
funcA |^ (m,n) ->  Subset of (E ^omega) equals :: FLANG_2:def 1
 union  {  B where B is Subset of (E ^omega) : ex k being Nat st
( m <= k &amp; k <= n &amp; B = A |^ k )  }  ;
coherence
 union  {  B where B is Subset of (E ^omega) : ex k being Nat st
( m <= k &amp; k <= n &amp; B = A |^ k )  }  is Subset of (E ^omega)
proofend;
end;

:: deftheorem  defines |^ FLANG_2:def_1_:_
 for E being set
for A being Subset of (E ^omega)
for m, n being Nat holds A |^ (m,n) = union  {  B where B is Subset of (E ^omega) : ex k being Nat st
( m <= k &amp; k <= n &amp; B = A |^ k )  }  ;

:: Union of a Range of Powers
:: Properties of |^ (n, m)
theorem Th19: :: FLANG_2:19
for E, x being set
for A being Subset of (E ^omega)
for m, n being Nat holds
( x in A |^ (m,n) iff ex k being Nat st
( m <= k &amp; k <= n &amp; x in A |^ k ) )
proofend;

theorem Th20: :: FLANG_2:20
for E being set
for A being Subset of (E ^omega)
for m, k, n being Nat st m <= k &amp; k <= n holds
A |^ k c= A |^ (m,n)
proofend;

theorem Th21: :: FLANG_2:21
for E being set
for A being Subset of (E ^omega)
for m, n being Nat holds
( A |^ (m,n) = {} iff ( m > n or ( m > 0 &amp; A = {} ) ) )
proofend;

theorem Th22: :: FLANG_2:22
for E being set
for A being Subset of (E ^omega)
for m being Nat holds A |^ (m,m) = A |^ m
proofend;

theorem Th23: :: FLANG_2:23
for E being set
for A being Subset of (E ^omega)
for m, k, l, n being Nat st m <= k &amp; l <= n holds
A |^ (k,l) c= A |^ (m,n)
proofend;

theorem :: FLANG_2:24
for E being set
for A being Subset of (E ^omega)
for m, k, n being Nat st m <= k &amp; k <= n holds
A |^ (m,n) = (A |^ (m,k)) \/ (A |^ (k,n))
proofend;

theorem Th25: :: FLANG_2:25
for E being set
for A being Subset of (E ^omega)
for m, k, n being Nat st m <= k &amp; k <= n holds
A |^ (m,n) = (A |^ (m,k)) \/ (A |^ ((k + 1),n))
proofend;

theorem Th26: :: FLANG_2:26
for E being set
for A being Subset of (E ^omega)
for m, n being Nat st m <= n + 1 holds
A |^ (m,(n + 1)) = (A |^ (m,n)) \/ (A |^ (n + 1))
proofend;

theorem :: FLANG_2:27
for E being set
for A being Subset of (E ^omega)
for m, n being Nat st m <= n holds
A |^ (m,n) = (A |^ m) \/ (A |^ ((m + 1),n))
proofend;

theorem Th28: :: FLANG_2:28
for E being set
for A being Subset of (E ^omega)
for n being Nat holds A |^ (n,(n + 1)) = (A |^ n) \/ (A |^ (n + 1))
proofend;

theorem Th29: :: FLANG_2:29
for E being set
for A, B being Subset of (E ^omega)
for m, n being Nat st A c= B holds
A |^ (m,n) c= B |^ (m,n)
proofend;

theorem Th30: :: FLANG_2:30
for x, E being set
for A being Subset of (E ^omega)
for m, n being Nat st x in A &amp; x <> <%> E &amp; ( m > 0 or n > 0 ) holds
A |^ (m,n) <> {(<%> E)}
proofend;

theorem Th31: :: FLANG_2:31
for E being set
for A being Subset of (E ^omega)
for m, n being Nat holds
( A |^ (m,n) = {(<%> E)} iff ( ( m <= n &amp; A = {(<%> E)} ) or ( m = 0 &amp; n = 0 ) or ( m = 0 &amp; A = {} ) ) )
proofend;

theorem Th32: :: FLANG_2:32
for E being set
for A being Subset of (E ^omega)
for m, n being Nat holds A |^ (m,n) c= A *
proofend;

theorem Th33: :: FLANG_2:33
for E being set
for A being Subset of (E ^omega)
for m, n being Nat holds
( <%> E in A |^ (m,n) iff ( m = 0 or ( m <= n &amp; <%> E in A ) ) )
proofend;

theorem Th34: :: FLANG_2:34
for E being set
for A being Subset of (E ^omega)
for m, n being Nat st <%> E in A &amp; m <= n holds
A |^ (m,n) = A |^ n
proofend;

theorem Th35: :: FLANG_2:35
for E being set
for A being Subset of (E ^omega)
for m, n, k being Nat holds (A |^ (m,n)) ^^ (A |^ k) = (A |^ k) ^^ (A |^ (m,n))
proofend;

theorem Th36: :: FLANG_2:36
for E being set
for A being Subset of (E ^omega)
for m, n being Nat holds (A |^ (m,n)) ^^ A = A ^^ (A |^ (m,n))
proofend;

theorem Th37: :: FLANG_2:37
for E being set
for A being Subset of (E ^omega)
for m, n, k, l being Nat st m <= n &amp; k <= l holds
(A |^ (m,n)) ^^ (A |^ (k,l)) = A |^ ((m + k),(n + l))
proofend;

theorem Th38: :: FLANG_2:38
for E being set
for A being Subset of (E ^omega)
for m, n being Nat holds A |^ ((m + 1),(n + 1)) = (A |^ (m,n)) ^^ A
proofend;

theorem Th39: :: FLANG_2:39
for E being set
for A being Subset of (E ^omega)
for m, n, k, l being Nat holds (A |^ (m,n)) ^^ (A |^ (k,l)) = (A |^ (k,l)) ^^ (A |^ (m,n))
proofend;

theorem Th40: :: FLANG_2:40
for E being set
for A being Subset of (E ^omega)
for m, n, k being Nat holds (A |^ (m,n)) |^ k = A |^ ((m * k),(n * k))
proofend;

theorem Th41: :: FLANG_2:41
for E being set
for A being Subset of (E ^omega)
for k, m, n being Nat holds (A |^ (k + 1)) |^ (m,n) c= ((A |^ k) |^ (m,n)) ^^ (A |^ (m,n))
proofend;

theorem Th42: :: FLANG_2:42
for E being set
for A being Subset of (E ^omega)
for k, m, n being Nat holds (A |^ k) |^ (m,n) c= A |^ ((k * m),(k * n))
proofend;

theorem :: FLANG_2:43
for E being set
for A being Subset of (E ^omega)
for k, m, n being Nat holds (A |^ k) |^ (m,n) c= (A |^ (m,n)) |^ k
proofend;

theorem :: FLANG_2:44
for E being set
for A being Subset of (E ^omega)
for k, l, m, n being Nat holds (A |^ (k + l)) |^ (m,n) c= ((A |^ k) |^ (m,n)) ^^ ((A |^ l) |^ (m,n))
proofend;

theorem Th45: :: FLANG_2:45
for E being set
for A being Subset of (E ^omega) holds A |^ (0,0) = {(<%> E)}
proofend;

theorem Th46: :: FLANG_2:46
for E being set
for A being Subset of (E ^omega) holds A |^ (0,1) = {(<%> E)} \/ A
proofend;

theorem :: FLANG_2:47
for E being set
for A being Subset of (E ^omega) holds A |^ (1,1) = A
proofend;

theorem :: FLANG_2:48
for E being set
for A being Subset of (E ^omega) holds A |^ (0,2) = ({(<%> E)} \/ A) \/ (A ^^ A)
proofend;

theorem :: FLANG_2:49
for E being set
for A being Subset of (E ^omega) holds A |^ (1,2) = A \/ (A ^^ A)
proofend;

theorem :: FLANG_2:50
for E being set
for A being Subset of (E ^omega) holds A |^ (2,2) = A ^^ A
proofend;

theorem Th51: :: FLANG_2:51
for E, x being set
for A being Subset of (E ^omega)
for m, n being Nat st m > 0 &amp; A |^ (m,n) = {x} holds
for mn being Nat st m <= mn &amp; mn <= n holds
A |^ mn = {x}
proofend;

theorem Th52: :: FLANG_2:52
for x, E being set
for A being Subset of (E ^omega)
for m, n being Nat st m <> n &amp; A |^ (m,n) = {x} holds
x = <%> E
proofend;

theorem Th53: :: FLANG_2:53
for x, E being set
for A being Subset of (E ^omega)
for m, n being Nat holds
( <%x%> in A |^ (m,n) iff ( <%x%> in A &amp; m <= n &amp; ( ( <%> E in A &amp; n > 0 ) or ( m <= 1 &amp; 1 <= n ) ) ) )
proofend;

theorem :: FLANG_2:54
for E being set
for A, B being Subset of (E ^omega)
for m, n being Nat holds (A /\ B) |^ (m,n) c= (A |^ (m,n)) /\ (B |^ (m,n))
proofend;

theorem :: FLANG_2:55
for E being set
for A, B being Subset of (E ^omega)
for m, n being Nat holds (A |^ (m,n)) \/ (B |^ (m,n)) c= (A \/ B) |^ (m,n)
proofend;

theorem :: FLANG_2:56
for E being set
for A being Subset of (E ^omega)
for m, n, k, l being Nat holds (A |^ (m,n)) |^ (k,l) c= A |^ ((m * k),(n * l))
proofend;

theorem :: FLANG_2:57
for E being set
for B, A being Subset of (E ^omega)
for m, n being Nat st m <= n &amp; <%> E in B holds
( A c= A ^^ (B |^ (m,n)) &amp; A c= (B |^ (m,n)) ^^ A )
proofend;

theorem :: FLANG_2:58
for E being set
for A, C, B being Subset of (E ^omega)
for m, n, k, l being Nat st m <= n &amp; k <= l &amp; A c= C |^ (m,n) &amp; B c= C |^ (k,l) holds
A ^^ B c= C |^ ((m + k),(n + l))
proofend;

theorem :: FLANG_2:59
for E being set
for A being Subset of (E ^omega)
for m, n being Nat holds (A |^ (m,n)) * c= A *
proofend;

theorem :: FLANG_2:60
for E being set
for A being Subset of (E ^omega)
for m, n being Nat holds (A *) |^ (m,n) c= A *
proofend;

theorem :: FLANG_2:61
for E being set
for A being Subset of (E ^omega)
for m, n being Nat st m <= n &amp; n > 0 holds
(A *) |^ (m,n) = A *
proofend;

theorem :: FLANG_2:62
for E being set
for A being Subset of (E ^omega)
for m, n being Nat st m <= n &amp; n > 0 &amp; <%> E in A holds
(A |^ (m,n)) * = A *
proofend;

theorem :: FLANG_2:63
for E being set
for A being Subset of (E ^omega)
for m, n being Nat st m <= n &amp; <%> E in A holds
(A |^ (m,n)) * = (A *) |^ (m,n)
proofend;

theorem Th64: :: FLANG_2:64
for E being set
for A, B being Subset of (E ^omega)
for m, n being Nat st A c= B * holds
A |^ (m,n) c= B *
proofend;

theorem :: FLANG_2:65
for E being set
for A, B being Subset of (E ^omega)
for m, n being Nat st A c= B * holds
B * = (B \/ (A |^ (m,n))) * by Th64, FLANG_1:67;

theorem Th66: :: FLANG_2:66
for E being set
for A being Subset of (E ^omega)
for m, n being Nat holds (A |^ (m,n)) ^^ (A *) = (A *) ^^ (A |^ (m,n))
proofend;

theorem :: FLANG_2:67
for E being set
for A being Subset of (E ^omega)
for m, n being Nat st <%> E in A &amp; m <= n holds
A * = (A *) ^^ (A |^ (m,n))
proofend;

theorem :: FLANG_2:68
for E being set
for A being Subset of (E ^omega)
for m, n, k being Nat holds (A |^ (m,n)) |^ k c= A * by Th32, FLANG_1:59;

theorem Th69: :: FLANG_2:69
for E being set
for A being Subset of (E ^omega)
for k, m, n being Nat holds (A |^ k) |^ (m,n) c= A *
proofend;

theorem :: FLANG_2:70
for E being set
for A being Subset of (E ^omega)
for m, n being Nat st m <= n holds
(A |^ m) * c= (A |^ (m,n)) * by Th20, FLANG_1:61;

theorem Th71: :: FLANG_2:71
for E being set
for A being Subset of (E ^omega)
for m, n, k, l being Nat holds (A |^ (m,n)) |^ (k,l) c= A *
proofend;

theorem Th72: :: FLANG_2:72
for E being set
for A being Subset of (E ^omega)
for k, n, l being Nat st <%> E in A &amp; k <= n &amp; l <= n holds
A |^ (k,n) = A |^ (l,n)
proofend;

begin

:: Optional Occurrence
:: Definition of ?
definition
let E be set ;
let A be Subset of (E ^omega);
funcA ?  ->  Subset of (E ^omega) equals :: FLANG_2:def 2
 union  {  B where B is Subset of (E ^omega) : ex k being Nat st
( k <= 1 &amp; B = A |^ k )  }  ;
coherence
 union  {  B where B is Subset of (E ^omega) : ex k being Nat st
( k <= 1 &amp; B = A |^ k )  }  is Subset of (E ^omega)
proofend;
end;

:: deftheorem  defines ? FLANG_2:def_2_:_
 for E being set
for A being Subset of (E ^omega) holds A ? = union  {  B where B is Subset of (E ^omega) : ex k being Nat st
( k <= 1 &amp; B = A |^ k )  }  ;

:: Optional Occurrence
:: Properties of ?
theorem Th73: :: FLANG_2:73
for E, x being set
for A being Subset of (E ^omega) holds
( x in A ? iff ex k being Nat st
( k <= 1 &amp; x in A |^ k ) )
proofend;

theorem :: FLANG_2:74
for E being set
for A being Subset of (E ^omega)
for n being Nat st n <= 1 holds
A |^ n c= A ?
proofend;

theorem Th75: :: FLANG_2:75
for E being set
for A being Subset of (E ^omega) holds A ? = (A |^ 0) \/ (A |^ 1)
proofend;

theorem Th76: :: FLANG_2:76
for E being set
for A being Subset of (E ^omega) holds A ? = {(<%> E)} \/ A
proofend;

theorem :: FLANG_2:77
for E being set
for A being Subset of (E ^omega) holds A c= A ?
proofend;

theorem Th78: :: FLANG_2:78
for x, E being set
for A being Subset of (E ^omega) holds
( x in A ? iff ( x = <%> E or x in A ) )
proofend;

theorem Th79: :: FLANG_2:79
for E being set
for A being Subset of (E ^omega) holds A ? = A |^ (0,1)
proofend;

theorem Th80: :: FLANG_2:80
for E being set
for A being Subset of (E ^omega) holds
( A ? = A iff <%> E in A )
proofend;

registration
let E be set ;
let A be Subset of (E ^omega);
clusterA ?  ->  non empty ;
coherence
 not A ? is empty
proofend;
end;

theorem :: FLANG_2:81
for E being set
for A being Subset of (E ^omega) holds (A ?) ? = A ?
proofend;

theorem :: FLANG_2:82
for E being set
for A, B being Subset of (E ^omega) st A c= B holds
A ? c= B ?
proofend;

theorem :: FLANG_2:83
for x, E being set
for A being Subset of (E ^omega) st x in A &amp; x <> <%> E holds
A ? <> {(<%> E)}
proofend;

theorem :: FLANG_2:84
for E being set
for A being Subset of (E ^omega) holds
( A ? = {(<%> E)} iff ( A = {} or A = {(<%> E)} ) )
proofend;

theorem :: FLANG_2:85
for E being set
for A being Subset of (E ^omega) holds
( (A *) ? = A * &amp; (A ?) * = A * )
proofend;

theorem :: FLANG_2:86
for E being set
for A being Subset of (E ^omega) holds A ? c= A *
proofend;

theorem :: FLANG_2:87
for E being set
for A, B being Subset of (E ^omega) holds (A /\ B) ? = (A ?) /\ (B ?)
proofend;

theorem :: FLANG_2:88
for E being set
for A, B being Subset of (E ^omega) holds (A ?) \/ (B ?) = (A \/ B) ?
proofend;

theorem :: FLANG_2:89
for x, E being set
for A being Subset of (E ^omega) st A ? = {x} holds
x = <%> E
proofend;

theorem :: FLANG_2:90
for E, x being set
for A being Subset of (E ^omega) holds
( <%x%> in A ? iff <%x%> in A )
proofend;

theorem :: FLANG_2:91
for E being set
for A being Subset of (E ^omega) holds (A ?) ^^ A = A ^^ (A ?)
proofend;

theorem :: FLANG_2:92
for E being set
for A being Subset of (E ^omega) holds (A ?) ^^ A = A |^ (1,2)
proofend;

theorem Th93: :: FLANG_2:93
for E being set
for A being Subset of (E ^omega) holds (A ?) ^^ (A ?) = A |^ (0,2)
proofend;

theorem Th94: :: FLANG_2:94
for E being set
for A being Subset of (E ^omega)
for k being Nat holds (A ?) |^ k = (A ?) |^ (0,k)
proofend;

theorem Th95: :: FLANG_2:95
for E being set
for A being Subset of (E ^omega)
for k being Nat holds (A ?) |^ k = A |^ (0,k)
proofend;

theorem Th96: :: FLANG_2:96
for E being set
for A being Subset of (E ^omega)
for m, n being Nat st m <= n holds
(A ?) |^ (m,n) = (A ?) |^ (0,n)
proofend;

theorem Th97: :: FLANG_2:97
for E being set
for A being Subset of (E ^omega)
for n being Nat holds (A ?) |^ (0,n) = A |^ (0,n)
proofend;

theorem Th98: :: FLANG_2:98
for E being set
for A being Subset of (E ^omega)
for m, n being Nat st m <= n holds
(A ?) |^ (m,n) = A |^ (0,n)
proofend;

theorem :: FLANG_2:99
for E being set
for A being Subset of (E ^omega)
for n being Nat holds (A |^ (1,n)) ? = A |^ (0,n)
proofend;

theorem :: FLANG_2:100
for E being set
for A, B being Subset of (E ^omega) st <%> E in A &amp; <%> E in B holds
( A ? c= A ^^ B &amp; A ? c= B ^^ A )
proofend;

theorem :: FLANG_2:101
for E being set
for A, B being Subset of (E ^omega) holds
( A c= A ^^ (B ?) &amp; A c= (B ?) ^^ A )
proofend;

theorem :: FLANG_2:102
for E being set
for A, C, B being Subset of (E ^omega) st A c= C ? &amp; B c= C ? holds
A ^^ B c= C |^ (0,2)
proofend;

theorem :: FLANG_2:103
for E being set
for A being Subset of (E ^omega)
for n being Nat st <%> E in A &amp; n > 0 holds
A ? c= A |^ n
proofend;

theorem :: FLANG_2:104
for E being set
for A being Subset of (E ^omega)
for k being Nat holds (A ?) ^^ (A |^ k) = (A |^ k) ^^ (A ?)
proofend;

theorem Th105: :: FLANG_2:105
for E being set
for A, B being Subset of (E ^omega) st A c= B * holds
A ? c= B *
proofend;

theorem :: FLANG_2:106
for E being set
for A, B being Subset of (E ^omega) st A c= B * holds
B * = (B \/ (A ?)) * by Th105, FLANG_1:67;

theorem :: FLANG_2:107
for E being set
for A being Subset of (E ^omega) holds (A ?) ^^ (A *) = (A *) ^^ (A ?)
proofend;

theorem :: FLANG_2:108
for E being set
for A being Subset of (E ^omega) holds (A ?) ^^ (A *) = A *
proofend;

theorem :: FLANG_2:109
for E being set
for A being Subset of (E ^omega)
for k being Nat holds (A ?) |^ k c= A *
proofend;

theorem :: FLANG_2:110
for E being set
for A being Subset of (E ^omega)
for k being Nat holds (A |^ k) ? c= A *
proofend;

theorem :: FLANG_2:111
for E being set
for A being Subset of (E ^omega)
for m, n being Nat holds (A ?) ^^ (A |^ (m,n)) = (A |^ (m,n)) ^^ (A ?)
proofend;

theorem :: FLANG_2:112
for E being set
for A being Subset of (E ^omega)
for k being Nat holds (A ?) ^^ (A |^ k) = A |^ (k,(k + 1))
proofend;

theorem :: FLANG_2:113
for E being set
for A being Subset of (E ^omega)
for m, n being Nat holds (A ?) |^ (m,n) c= A *
proofend;

theorem :: FLANG_2:114
for E being set
for A being Subset of (E ^omega)
for m, n being Nat holds (A |^ (m,n)) ? c= A *
proofend;

theorem :: FLANG_2:115
for E being set
for A being Subset of (E ^omega) holds A ? = (A \ {(<%> E)}) ?
proofend;

theorem :: FLANG_2:116
for E being set
for A, B being Subset of (E ^omega) st A c= B ? holds
A ? c= B ?
proofend;

theorem :: FLANG_2:117
for E being set
for A, B being Subset of (E ^omega) st A c= B ? holds
B ? = (B \/ A) ?
proofend;