:: FLANG_2 semantic presentation

begin


theorem Th1: :: FLANG_2:1
for m, k, i, n being Nat st m + k <= i & i <= n + k holds
ex mn being Nat st
( mn + k = i & m <= mn & mn <= n )
proof
let m, k, i, n be Nat; ::_thesis: ( m + k <= i & i <= n + k implies ex mn being Nat st
( mn + k = i & m <= mn & mn <= n ) )
assume that
A1: m + k <= i and
A2: i <= n + k ; ::_thesis: ex mn being Nat st
( mn + k = i & m <= mn & mn <= n )
 m + k <= m + i by A1, XREAL_1:38;
then  k <= i by XREAL_1:6;
then reconsider mn = i - k as Nat by NAT_1:21;
take  mn ; ::_thesis: ( mn + k = i & m <= mn & mn <= n )
thus  mn + k = i ; ::_thesis: ( m <= mn & mn <= n )
 m + k <= mn + k by A1;
hence  ( m <= mn & mn <= n ) by A2, XREAL_1:6; ::_thesis: verum
end;

theorem Th2: :: FLANG_2:2
for m, n, k, l, i being Nat st m <= n & k <= l & m + k <= i & i <= n + l holds
ex mn, kl being Nat st
( mn + kl = i & m <= mn & mn <= n & k <= kl & kl <= l )
proof
let m, n, k, l, i be Nat; ::_thesis: ( m <= n & k <= l & m + k <= i & i <= n + l implies ex mn, kl being Nat st
( mn + kl = i & m <= mn & mn <= n & k <= kl & kl <= l ) )
assume that
A1: m <= n and
A2: k <= l and
A3: m + k <= i and
A4: i <= n + l ; ::_thesis: ex mn, kl being Nat st
( mn + kl = i & m <= mn & mn <= n & k <= kl & kl <= l )
percases ( i <= n + k or i > n + k ) ;
suppose i <= n + k ; ::_thesis: ex mn, kl being Nat st
( mn + kl = i & m <= mn & mn <= n & k <= kl & kl <= l )
then consider mn being Nat such that
A5: ( mn + k = i & m <= mn & mn <= n ) by A3, Th1;
take  mn ; ::_thesis: ex kl being Nat st
( mn + kl = i & m <= mn & mn <= n & k <= kl & kl <= l )
take  k ; ::_thesis: ( mn + k = i & m <= mn & mn <= n & k <= k & k <= l )
thus  ( mn + k = i & m <= mn & mn <= n ) by A5; ::_thesis: ( k <= k & k <= l )
thus  ( k <= k & k <= l ) by A2; ::_thesis: verum
end;
suppose i > n + k ; ::_thesis: ex mn, kl being Nat st
( mn + kl = i & m <= mn & mn <= n & k <= kl & kl <= l )
then consider kl being Nat such that
A6: kl + n = i and
A7: ( k <= kl & kl <= l ) by A4, Th1;
take  n ; ::_thesis: ex kl being Nat st
( n + kl = i & m <= n & n <= n & k <= kl & kl <= l )
take  kl ; ::_thesis: ( n + kl = i & m <= n & n <= n & k <= kl & kl <= l )
thus  ( n + kl = i & m <= n & n <= n ) by A1, A6; ::_thesis: ( k <= kl & kl <= l )
thus  ( k <= kl & kl <= l ) by A7; ::_thesis: verum
end;
end;
end;

theorem Th3: :: FLANG_2:3
for m, n being Nat st m < n holds
ex k being Nat st
( m + k = n & k > 0 )
proof
let m, n be Nat; ::_thesis: ( m < n implies ex k being Nat st
( m + k = n & k > 0 ) )
assume  m < n ; ::_thesis: ex k being Nat st
( m + k = n & k > 0 )
then  ( ex k being Nat st m + k = n & m - m < n - m ) by NAT_1:10, XREAL_1:14;
hence  ex k being Nat st
( m + k = n & k > 0 ) ; ::_thesis: verum
end;

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 = {}
proof
let E be set ; ::_thesis: for a, b being Element of E ^omega st ( a ^ b = a or b ^ a = a ) holds
b = {}
let a, b be Element of E ^omega ; ::_thesis: ( ( a ^ b = a or b ^ a = a ) implies b = {} )
assume A1: ( a ^ b = a or b ^ a = a ) ; ::_thesis: b = {}
percases ( a ^ b = a or b ^ a = a ) by A1;
supposeA2: a ^ b = a ; ::_thesis: b = {}
 len (a ^ b) = (len a) + (len b) by AFINSQ_1:17;
hence  b = {} by A2; ::_thesis: verum
end;
supposeA3: b ^ a = a ; ::_thesis: b = {}
 len (b ^ a) = (len b) + (len a) by AFINSQ_1:17;
hence  b = {} by A3; ::_thesis: verum
end;
end;
end;

begin

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 ) & x <> <%> E holds
A ^^ B <> {(<%> E)}
proof
let x, E be set ; ::_thesis: for A, B being Subset of (E ^omega) st ( x in A or x in B ) & x <> <%> E holds
A ^^ B <> {(<%> E)}
let A, B be Subset of (E ^omega); ::_thesis: ( ( x in A or x in B ) & x <> <%> E implies A ^^ B <> {(<%> E)} )
assume  ( ( x in A or x in B ) & x <> <%> E ) ; ::_thesis: A ^^ B <> {(<%> E)}
then  ( A <> {(<%> E)} or B <> {(<%> E)} ) by TARSKI:def_1;
hence  A ^^ B <> {(<%> E)} by FLANG_1:14; ::_thesis: verum
end;

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 & <%x%> in B ) or ( <%x%> in A & <%> E in B ) ) )
proof
let x, E be set ; ::_thesis: for A, B being Subset of (E ^omega) holds
( <%x%> in A ^^ B iff ( ( <%> E in A & <%x%> in B ) or ( <%x%> in A & <%> E in B ) ) )
let A, B be Subset of (E ^omega); ::_thesis: ( <%x%> in A ^^ B iff ( ( <%> E in A & <%x%> in B ) or ( <%x%> in A & <%> E in B ) ) )
thus  ( not <%x%> in A ^^ B or ( <%> E in A & <%x%> in B ) or ( <%x%> in A & <%> E in B ) ) ::_thesis: ( ( ( <%> E in A & <%x%> in B ) or ( <%x%> in A & <%> E in B ) ) implies <%x%> in A ^^ B )
proof
assume  <%x%> in A ^^ B ; ::_thesis: ( ( <%> E in A & <%x%> in B ) or ( <%x%> in A & <%> E in B ) )
then  ex a, b being Element of E ^omega st
( a in A & b in B & <%x%> = a ^ b ) by FLANG_1:def_1;
hence  ( ( <%> E in A & <%x%> in B ) or ( <%x%> in A & <%> E in B ) ) by FLANG_1:4; ::_thesis: verum
end;
A1: ( {} ^ <%x%> = <%x%> & <%x%> ^ {} = <%x%> ) ;
assume  ( ( <%> E in A & <%x%> in B ) or ( <%x%> in A & <%> E in B ) ) ; ::_thesis: <%x%> in A ^^ B
hence  <%x%> in A ^^ B by A1, FLANG_1:def_1; ::_thesis: verum
end;

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 & x <> <%> E & n > 0 holds
A |^ n <> {(<%> E)}
proof
let x, E be set ; ::_thesis: for A being Subset of (E ^omega)
for n being Nat st x in A & x <> <%> E & n > 0 holds
A |^ n <> {(<%> E)}
let A be Subset of (E ^omega); ::_thesis: for n being Nat st x in A & x <> <%> E & n > 0 holds
A |^ n <> {(<%> E)}
let n be Nat; ::_thesis: ( x in A & x <> <%> E & n > 0 implies A |^ n <> {(<%> E)} )
assume that
A1: ( x in A & x <> <%> E ) and
A2: n > 0 ; ::_thesis: A |^ n <> {(<%> E)}
 A <> {(<%> E)} by A1, TARSKI:def_1;
hence  A |^ n <> {(<%> E)} by A2, FLANG_1:29; ::_thesis: verum
end;

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 ) )
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for n being Nat holds
( <%> E in A |^ n iff ( n = 0 or <%> E in A ) )
let A be Subset of (E ^omega); ::_thesis: for n being Nat holds
( <%> E in A |^ n iff ( n = 0 or <%> E in A ) )
let n be Nat; ::_thesis: ( <%> E in A |^ n iff ( n = 0 or <%> E in A ) )
thus  ( not <%> E in A |^ n or n = 0 or <%> E in A ) by FLANG_1:31; ::_thesis: ( ( n = 0 or <%> E in A ) implies <%> E in A |^ n )
assume A1: ( n = 0 or <%> E in A ) ; ::_thesis: <%> E in A |^ n
percases ( n = 0 or <%> E in A ) by A1;
suppose n = 0 ; ::_thesis: <%> E in A |^ n
then  A |^ n = {(<%> E)} by FLANG_1:29;
hence  <%> E in A |^ n by ZFMISC_1:31; ::_thesis: verum
end;
suppose <%> E in A ; ::_thesis: <%> E in A |^ n
hence  <%> E in A |^ n by FLANG_1:30; ::_thesis: verum
end;
end;
end;

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 & ( ( <%> E in A & n > 1 ) or n = 1 ) ) )
proof
let x, E be set ; ::_thesis: for A being Subset of (E ^omega)
for n being Nat holds
( <%x%> in A |^ n iff ( <%x%> in A & ( ( <%> E in A & n > 1 ) or n = 1 ) ) )
let A be Subset of (E ^omega); ::_thesis: for n being Nat holds
( <%x%> in A |^ n iff ( <%x%> in A & ( ( <%> E in A & n > 1 ) or n = 1 ) ) )
let n be Nat; ::_thesis: ( <%x%> in A |^ n iff ( <%x%> in A & ( ( <%> E in A & n > 1 ) or n = 1 ) ) )
thus  ( <%x%> in A |^ n implies ( <%x%> in A & ( ( <%> E in A & n > 1 ) or n = 1 ) ) ) ::_thesis: ( <%x%> in A & ( ( <%> E in A & n > 1 ) or n = 1 ) implies <%x%> in A |^ n )
proof
assume A1: <%x%> in A |^ n ; ::_thesis: ( <%x%> in A & ( ( <%> E in A & n > 1 ) or n = 1 ) )
 A |^ n c= A * by FLANG_1:42;
hence  <%x%> in A by A1, FLANG_1:72; ::_thesis: ( ( <%> E in A & n > 1 ) or n = 1 )
assume A2: ( ( not <%> E in A or n <= 1 ) & n <> 1 ) ; ::_thesis: contradiction
percases ( ( not <%> E in A & n <> 1 ) or ( n <= 1 & n <> 1 ) ) by A2;
supposeA3: ( not <%> E in A & n <> 1 ) ; ::_thesis: contradiction
percases ( n = 0 or n > 1 ) by A3, NAT_1:25;
suppose n = 0 ; ::_thesis: contradiction
then  A |^ n = {(<%> E)} by FLANG_1:24;
hence  contradiction by A1, TARSKI:def_1; ::_thesis: verum
end;
supposeA4: n > 1 ; ::_thesis: contradiction
then consider m being Nat such that
A5: m + 1 = n by NAT_1:6;
 <%x%> in (A |^ m) ^^ A by A1, A5, FLANG_1:23;
then consider a, b being Element of E ^omega  such that
A6: a in A |^ m and
A7: b in A and
A8: <%x%> = a ^ b by FLANG_1:def_1;
percases ( ( a = <%> E & b = <%x%> ) or ( b = <%> E & a = <%x%> ) ) by A8, FLANG_1:4;
supposeA9: ( a = <%> E & b = <%x%> ) ; ::_thesis: contradiction
 m + 1 > 0 + 1 by A4, A5;
then  m > 0 ;
hence  contradiction by A3, A6, A9, FLANG_1:31; ::_thesis: verum
end;
suppose ( b = <%> E & a = <%x%> ) ; ::_thesis: contradiction
hence  contradiction by A3, A7; ::_thesis: verum
end;
end;
end;
end;
end;
suppose ( n <= 1 & n <> 1 ) ; ::_thesis: contradiction
then  n = 0 by NAT_1:25;
then  A |^ n = {(<%> E)} by FLANG_1:24;
hence  contradiction by A1, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
assume that
A10: <%x%> in A and
A11: ( ( <%> E in A & n > 1 ) or n = 1 ) ; ::_thesis: <%x%> in A |^ n
percases ( ( <%> E in A & n > 1 ) or n = 1 ) by A11;
suppose ( <%> E in A & n > 1 ) ; ::_thesis: <%x%> in A |^ n
then  A c= A |^ n by FLANG_1:35;
hence  <%x%> in A |^ n by A10; ::_thesis: verum
end;
suppose n = 1 ; ::_thesis: <%x%> in A |^ n
hence  <%x%> in A |^ n by A10, FLANG_1:25; ::_thesis: verum
end;
end;
end;

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 & A |^ m = {x} & A |^ n = {x} holds
x = <%> E
proof
let x, E be set ; ::_thesis: for A being Subset of (E ^omega)
for m, n being Nat st m <> n & A |^ m = {x} & A |^ n = {x} holds
x = <%> E
let A be Subset of (E ^omega); ::_thesis: for m, n being Nat st m <> n & A |^ m = {x} & A |^ n = {x} holds
x = <%> E
let m, n be Nat; ::_thesis: ( m <> n & A |^ m = {x} & A |^ n = {x} implies x = <%> E )
assume that
A1: m <> n and
A2: A |^ m = {x} and
A3: A |^ n = {x} ; ::_thesis: x = <%> E
A4: x in A |^ m by A2, TARSKI:def_1;
A5: x in A |^ n by A3, TARSKI:def_1;
percases ( m > n or m < n ) by A1, XXREAL_0:1;
suppose m > n ; ::_thesis: x = <%> E
then consider k being Nat such that
A6: n + k = m and
A7: k > 0 by Th3;
 (A |^ n) ^^ (A |^ k) = A |^ m by A6, FLANG_1:33;
then consider a, b being Element of E ^omega  such that
A8: a in A |^ n and
A9: b in A |^ k and
A10: x = a ^ b by A4, FLANG_1:def_1;
 a = x by A3, A8, TARSKI:def_1;
then  b = <%> E by A10, Th4;
then  <%> E in A by A7, A9, FLANG_1:31;
then  <%> E in A |^ m by FLANG_1:30;
hence  x = <%> E by A2, TARSKI:def_1; ::_thesis: verum
end;
suppose m < n ; ::_thesis: x = <%> E
then consider k being Nat such that
A11: m + k = n and
A12: k > 0 by Th3;
 (A |^ m) ^^ (A |^ k) = A |^ n by A11, FLANG_1:33;
then consider a, b being Element of E ^omega  such that
A13: a in A |^ m and
A14: b in A |^ k and
A15: x = a ^ b by A5, FLANG_1:def_1;
 a = x by A2, A13, TARSKI:def_1;
then  b = <%> E by A15, Th4;
then  <%> E in A by A12, A14, FLANG_1:31;
then  <%> E in A |^ m by FLANG_1:30;
hence  x = <%> E by A2, TARSKI:def_1; ::_thesis: verum
end;
end;
end;

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
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for m, n being Nat holds (A |^ m) |^ n = (A |^ n) |^ m
let A be Subset of (E ^omega); ::_thesis: for m, n being Nat holds (A |^ m) |^ n = (A |^ n) |^ m
let m, n be Nat; ::_thesis: (A |^ m) |^ n = (A |^ n) |^ m
thus (A |^ m) |^ n = A |^ (m * n) by FLANG_1:34
.= (A |^ n) |^ m by FLANG_1:34 ; ::_thesis: verum
end;

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)
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for m, n being Nat holds (A |^ m) ^^ (A |^ n) = (A |^ n) ^^ (A |^ m)
let A be Subset of (E ^omega); ::_thesis: for m, n being Nat holds (A |^ m) ^^ (A |^ n) = (A |^ n) ^^ (A |^ m)
let m, n be Nat; ::_thesis: (A |^ m) ^^ (A |^ n) = (A |^ n) ^^ (A |^ m)
thus (A |^ m) ^^ (A |^ n) = A |^ (m + n) by FLANG_1:33
.= (A |^ n) ^^ (A |^ m) by FLANG_1:33 ; ::_thesis: verum
end;

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) & A c= (B |^ l) ^^ A )
proof
let E be set ; ::_thesis: for B, A being Subset of (E ^omega)
for l being Nat st <%> E in B holds
( A c= A ^^ (B |^ l) & A c= (B |^ l) ^^ A )
let B, A be Subset of (E ^omega); ::_thesis: for l being Nat st <%> E in B holds
( A c= A ^^ (B |^ l) & A c= (B |^ l) ^^ A )
let l be Nat; ::_thesis: ( <%> E in B implies ( A c= A ^^ (B |^ l) & A c= (B |^ l) ^^ A ) )
assume  <%> E in B ; ::_thesis: ( A c= A ^^ (B |^ l) & A c= (B |^ l) ^^ A )
then  <%> E in B |^ l by FLANG_1:30;
hence  ( A c= A ^^ (B |^ l) & A c= (B |^ l) ^^ A ) by FLANG_1:16; ::_thesis: verum
end;

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 & B c= C |^ l holds
A ^^ B c= C |^ (k + l)
proof
let E be set ; ::_thesis: for A, C, B being Subset of (E ^omega)
for k, l being Nat st A c= C |^ k & B c= C |^ l holds
A ^^ B c= C |^ (k + l)
let A, C, B be Subset of (E ^omega); ::_thesis: for k, l being Nat st A c= C |^ k & B c= C |^ l holds
A ^^ B c= C |^ (k + l)
let k, l be Nat; ::_thesis: ( A c= C |^ k & B c= C |^ l implies A ^^ B c= C |^ (k + l) )
assume  ( A c= C |^ k & B c= C |^ l ) ; ::_thesis: A ^^ B c= C |^ (k + l)
then  A ^^ B c= (C |^ k) ^^ (C |^ l) by FLANG_1:17;
hence  A ^^ B c= C |^ (k + l) by FLANG_1:33; ::_thesis: verum
end;

theorem :: FLANG_2:15
for x, E being set
for A being Subset of (E ^omega) st x in A & x <> <%> E holds
A * <> {(<%> E)}
proof
let x, E be set ; ::_thesis: for A being Subset of (E ^omega) st x in A & x <> <%> E holds
A * <> {(<%> E)}
let A be Subset of (E ^omega); ::_thesis: ( x in A & x <> <%> E implies A * <> {(<%> E)} )
assume that
A1: x in A and
A2: x <> <%> E ; ::_thesis: A * <> {(<%> E)}
 A <> {(<%> E)} by A1, A2, TARSKI:def_1;
hence  A * <> {(<%> E)} by A1, FLANG_1:47; ::_thesis: verum
end;

theorem Th16: :: FLANG_2:16
for E being set
for A being Subset of (E ^omega)
for n being Nat st <%> E in A & n > 0 holds
(A |^ n) * = A *
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for n being Nat st <%> E in A & n > 0 holds
(A |^ n) * = A *
let A be Subset of (E ^omega); ::_thesis: for n being Nat st <%> E in A & n > 0 holds
(A |^ n) * = A *
let n be Nat; ::_thesis: ( <%> E in A & n > 0 implies (A |^ n) * = A * )
assume  ( <%> E in A & n > 0 ) ; ::_thesis: (A |^ n) * = A *
then A1: A * c= (A |^ n) * by FLANG_1:35, FLANG_1:61;
 (A |^ n) * c= A * by FLANG_1:64;
hence  (A |^ n) * = A * by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

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
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for n being Nat st <%> E in A holds
(A |^ n) * = (A *) |^ n
let A be Subset of (E ^omega); ::_thesis: for n being Nat st <%> E in A holds
(A |^ n) * = (A *) |^ n
let n be Nat; ::_thesis: ( <%> E in A implies (A |^ n) * = (A *) |^ n )
assume A1: <%> E in A ; ::_thesis: (A |^ n) * = (A *) |^ n
percases ( n = 0 or n > 0 ) ;
supposeA2: n = 0 ; ::_thesis: (A |^ n) * = (A *) |^ n
hence (A |^ n) * = {(<%> E)} * by FLANG_1:24
.= {(<%> E)} by FLANG_1:47
.= (A *) |^ n by A2, FLANG_1:24 ;
::_thesis: verum
end;
supposeA3: n > 0 ; ::_thesis: (A |^ n) * = (A *) |^ n
then  (A *) |^ n = A * by FLANG_1:66;
hence  (A |^ n) * = (A *) |^ n by A1, A3, Th16; ::_thesis: verum
end;
end;
end;

theorem :: FLANG_2:18
for E being set
for A, B being Subset of (E ^omega) holds
( A c= A ^^ (B *) & A c= (B *) ^^ A )
proof
let E be set ; ::_thesis: for A, B being Subset of (E ^omega) holds
( A c= A ^^ (B *) & A c= (B *) ^^ A )
let A, B be Subset of (E ^omega); ::_thesis: ( A c= A ^^ (B *) & A c= (B *) ^^ A )
 <%> E in B * by FLANG_1:48;
hence  ( A c= A ^^ (B *) & A c= (B *) ^^ A ) by FLANG_1:16; ::_thesis: verum
end;

begin

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 & k <= n & B = A |^ k )  }  ;
coherence
 union  {  B where B is Subset of (E ^omega) : ex k being Nat st
( m <= k & k <= n & B = A |^ k )  }  is Subset of (E ^omega)
proof
defpred S1[ set ] means  ex k being Nat st
( m <= k & k <= n & $1 = A |^ k );
reconsider M =  {  B where B is Subset of (E ^omega) : S1[B]  }  as Subset-Family of (E ^omega) from DOMAIN_1:sch_7();
 union M is Subset of (E ^omega) ;
hence  union  {  B where B is Subset of (E ^omega) : ex k being Nat st
( m <= k & k <= n & B = A |^ k )  }  is Subset of (E ^omega) ; ::_thesis: verum
end;
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 & k <= n & B = A |^ k )  }  ;

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 & k <= n & x in A |^ k ) )
proof
let E, x be set ; ::_thesis: 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 & k <= n & x in A |^ k ) )
let A be Subset of (E ^omega); ::_thesis: for m, n being Nat holds
( x in A |^ (m,n) iff ex k being Nat st
( m <= k & k <= n & x in A |^ k ) )
let m, n be Nat; ::_thesis: ( x in A |^ (m,n) iff ex k being Nat st
( m <= k & k <= n & x in A |^ k ) )
thus  ( x in A |^ (m,n) implies ex k being Nat st
( m <= k & k <= n & x in A |^ k ) ) ::_thesis: ( ex k being Nat st
( m <= k & k <= n & x in A |^ k ) implies x in A |^ (m,n) )
proof
defpred S1[ set ] means  ex k being Nat st
( m <= k & k <= n & $1 = A |^ k );
assume  x in A |^ (m,n) ; ::_thesis: ex k being Nat st
( m <= k & k <= n & x in A |^ k )
then consider X being set  such that
A1: x in X and
A2: X in  {  B where B is Subset of (E ^omega) : ex k being Nat st
( m <= k & k <= n & B = A |^ k )  }  by TARSKI:def_4;
A3: X in  {  B where B is Subset of (E ^omega) : S1[B]  }  by A2;
 S1[X] from CARD_FIL:sch_1(A3);
hence  ex k being Nat st
( m <= k & k <= n & x in A |^ k ) by A1; ::_thesis: verum
end;
given k being Nat such that A4: ( m <= k & k <= n & x in A |^ k ) ; ::_thesis: x in A |^ (m,n)
defpred S1[ set ] means  ex k being Nat st
( m <= k & k <= n & $1 = A |^ k );
consider B being Subset of (E ^omega) such that
A5: x in B and
A6: S1[B] by A4;
reconsider A =  {  C where C is Subset of (E ^omega) : S1[C]  }  as Subset-Family of (E ^omega) from DOMAIN_1:sch_7();
 B in A by A6;
hence  x in A |^ (m,n) by A5, TARSKI:def_4; ::_thesis: verum
end;

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 & k <= n holds
A |^ k c= A |^ (m,n)
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for m, k, n being Nat st m <= k & k <= n holds
A |^ k c= A |^ (m,n)
let A be Subset of (E ^omega); ::_thesis: for m, k, n being Nat st m <= k & k <= n holds
A |^ k c= A |^ (m,n)
let m, k, n be Nat; ::_thesis: ( m <= k & k <= n implies A |^ k c= A |^ (m,n) )
assume  ( m <= k & k <= n ) ; ::_thesis: A |^ k c= A |^ (m,n)
then  for x being set st x in A |^ k holds
x in A |^ (m,n) by Th19;
hence  A |^ k c= A |^ (m,n) by TARSKI:def_3; ::_thesis: verum
end;

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 & A = {} ) ) )
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for m, n being Nat holds
( A |^ (m,n) = {} iff ( m > n or ( m > 0 & A = {} ) ) )
let A be Subset of (E ^omega); ::_thesis: for m, n being Nat holds
( A |^ (m,n) = {} iff ( m > n or ( m > 0 & A = {} ) ) )
let m, n be Nat; ::_thesis: ( A |^ (m,n) = {} iff ( m > n or ( m > 0 & A = {} ) ) )
A1: now__::_thesis:_(_m_>_0_&_A_=_{}_implies_A_|^_(m,n)_=_{}_)
assume A2: ( m > 0 & A = {} ) ; ::_thesis: A |^ (m,n) = {}
now__::_thesis:_for_x_being_set_holds_not_x_in_A_|^_(m,n)
let x be set ; ::_thesis: not x in A |^ (m,n)
assume  x in A |^ (m,n) ; ::_thesis: contradiction
then  ex k being Nat st
( m <= k & k <= n & x in A |^ k ) by Th19;
hence  contradiction by A2, FLANG_1:27; ::_thesis: verum
end;
hence  A |^ (m,n) = {} by XBOOLE_0:def_1; ::_thesis: verum
end;
thus  ( not A |^ (m,n) = {} or m > n or ( m > 0 & A = {} ) ) ::_thesis: ( ( m > n or ( m > 0 & A = {} ) ) implies A |^ (m,n) = {} )
proof
assume that
A3: A |^ (m,n) = {} and
A4: ( m <= n & ( m <= 0 or A <> {} ) ) ; ::_thesis: contradiction
A5: now__::_thesis:_(_m_<=_n_implies_not_A_<>_{}_)
assume that
A6: m <= n and
A7: A <> {} ; ::_thesis: contradiction
 A |^ m <> {} by A7, FLANG_1:27;
then  ex a being Element of E ^omega st a in A |^ m by SUBSET_1:4;
hence  contradiction by A3, A6, Th19; ::_thesis: verum
end;
now__::_thesis:_(_m_<=_n_implies_not_m_=_0_)
assume that
A8: m <= n and
A9: m = 0 ; ::_thesis: contradiction
 {(<%> E)} = A |^ m by A9, FLANG_1:29;
then  <%> E in A |^ m by TARSKI:def_1;
hence  contradiction by A3, A8, Th19; ::_thesis: verum
end;
hence  contradiction by A4, A5; ::_thesis: verum
end;
now__::_thesis:_(_m_>_n_implies_A_|^_(m,n)_=_{}_)
assume A10: m > n ; ::_thesis: A |^ (m,n) = {}
now__::_thesis:_for_x_being_set_holds_not_x_in_A_|^_(m,n)
let x be set ; ::_thesis: not x in A |^ (m,n)
 for k being Nat holds
( not m <= k or not k <= n or not x in A |^ k ) by A10, XXREAL_0:2;
hence  not x in A |^ (m,n) by Th19; ::_thesis: verum
end;
hence  A |^ (m,n) = {} by XBOOLE_0:def_1; ::_thesis: verum
end;
hence  ( ( m > n or ( m > 0 & A = {} ) ) implies A |^ (m,n) = {} ) by A1; ::_thesis: verum
end;

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
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for m being Nat holds A |^ (m,m) = A |^ m
let A be Subset of (E ^omega); ::_thesis: for m being Nat holds A |^ (m,m) = A |^ m
let m be Nat; ::_thesis: A |^ (m,m) = A |^ m
A1: now__::_thesis:_for_x_being_set_st_x_in_A_|^_(m,m)_holds_
x_in_A_|^_m
let x be set ; ::_thesis: ( x in A |^ (m,m) implies x in A |^ m )
assume  x in A |^ (m,m) ; ::_thesis: x in A |^ m
then  ex k being Nat st
( m <= k & k <= m & x in A |^ k ) by Th19;
hence  x in A |^ m by XXREAL_0:1; ::_thesis: verum
end;
 for x being set st x in A |^ m holds
x in A |^ (m,m) by Th19;
hence  A |^ (m,m) = A |^ m by A1, TARSKI:1; ::_thesis: verum
end;

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 & l <= n holds
A |^ (k,l) c= A |^ (m,n)
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for m, k, l, n being Nat st m <= k & l <= n holds
A |^ (k,l) c= A |^ (m,n)
let A be Subset of (E ^omega); ::_thesis: for m, k, l, n being Nat st m <= k & l <= n holds
A |^ (k,l) c= A |^ (m,n)
let m, k, l, n be Nat; ::_thesis: ( m <= k & l <= n implies A |^ (k,l) c= A |^ (m,n) )
assume A1: ( m <= k & l <= n ) ; ::_thesis: A |^ (k,l) c= A |^ (m,n)
thus  A |^ (k,l) c= A |^ (m,n) ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A |^ (k,l) or x in A |^ (m,n) )
assume  x in A |^ (k,l) ; ::_thesis: x in A |^ (m,n)
then consider kl being Nat such that
A2: ( k <= kl & kl <= l ) and
A3: x in A |^ kl by Th19;
 ( m <= kl & kl <= n ) by A1, A2, XXREAL_0:2;
hence  x in A |^ (m,n) by A3, Th19; ::_thesis: verum
end;
end;

theorem :: FLANG_2:24
for E being set
for A being Subset of (E ^omega)
for m, k, n being Nat st m <= k & k <= n holds
A |^ (m,n) = (A |^ (m,k)) \/ (A |^ (k,n))
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for m, k, n being Nat st m <= k & k <= n holds
A |^ (m,n) = (A |^ (m,k)) \/ (A |^ (k,n))
let A be Subset of (E ^omega); ::_thesis: for m, k, n being Nat st m <= k & k <= n holds
A |^ (m,n) = (A |^ (m,k)) \/ (A |^ (k,n))
let m, k, n be Nat; ::_thesis: ( m <= k & k <= n implies A |^ (m,n) = (A |^ (m,k)) \/ (A |^ (k,n)) )
A1: A |^ (m,n) c= (A |^ (m,k)) \/ (A |^ (k,n))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A |^ (m,n) or x in (A |^ (m,k)) \/ (A |^ (k,n)) )
assume  x in A |^ (m,n) ; ::_thesis: x in (A |^ (m,k)) \/ (A |^ (k,n))
then consider l being Nat such that
A2: ( m <= l & l <= n & x in A |^ l ) by Th19;
 ( l <= k or l > k ) ;
then  ( x in A |^ (m,k) or x in A |^ (k,n) ) by A2, Th19;
hence  x in (A |^ (m,k)) \/ (A |^ (k,n)) by XBOOLE_0:def_3; ::_thesis: verum
end;
assume  ( m <= k & k <= n ) ; ::_thesis: A |^ (m,n) = (A |^ (m,k)) \/ (A |^ (k,n))
then  ( A |^ (m,k) c= A |^ (m,n) & A |^ (k,n) c= A |^ (m,n) ) by Th23;
then  (A |^ (m,k)) \/ (A |^ (k,n)) c= A |^ (m,n) by XBOOLE_1:8;
hence  A |^ (m,n) = (A |^ (m,k)) \/ (A |^ (k,n)) by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

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 & k <= n holds
A |^ (m,n) = (A |^ (m,k)) \/ (A |^ ((k + 1),n))
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for m, k, n being Nat st m <= k & k <= n holds
A |^ (m,n) = (A |^ (m,k)) \/ (A |^ ((k + 1),n))
let A be Subset of (E ^omega); ::_thesis: for m, k, n being Nat st m <= k & k <= n holds
A |^ (m,n) = (A |^ (m,k)) \/ (A |^ ((k + 1),n))
let m, k, n be Nat; ::_thesis: ( m <= k & k <= n implies A |^ (m,n) = (A |^ (m,k)) \/ (A |^ ((k + 1),n)) )
assume that
A1: m <= k and
A2: k <= n ; ::_thesis: A |^ (m,n) = (A |^ (m,k)) \/ (A |^ ((k + 1),n))
percases ( k < n or k >= n ) ;
supposeA3: k < n ; ::_thesis: A |^ (m,n) = (A |^ (m,k)) \/ (A |^ ((k + 1),n))
 m <= k + 1 by A1, NAT_1:13;
then A4: A |^ ((k + 1),n) c= A |^ (m,n) by Th23;
A5: A |^ (m,n) c= (A |^ (m,k)) \/ (A |^ ((k + 1),n))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A |^ (m,n) or x in (A |^ (m,k)) \/ (A |^ ((k + 1),n)) )
assume  x in A |^ (m,n) ; ::_thesis: x in (A |^ (m,k)) \/ (A |^ ((k + 1),n))
then consider mn being Nat such that
A6: m <= mn and
A7: mn <= n and
A8: x in A |^ mn by Th19;
A9: ( mn >= k + 1 implies x in A |^ ((k + 1),n) ) by A7, A8, Th19;
 ( mn <= k implies x in A |^ (m,k) ) by A6, A8, Th19;
hence  x in (A |^ (m,k)) \/ (A |^ ((k + 1),n)) by A9, NAT_1:13, XBOOLE_0:def_3; ::_thesis: verum
end;
 A |^ (m,k) c= A |^ (m,n) by A3, Th23;
then  (A |^ (m,k)) \/ (A |^ ((k + 1),n)) c= A |^ (m,n) by A4, XBOOLE_1:8;
hence  A |^ (m,n) = (A |^ (m,k)) \/ (A |^ ((k + 1),n)) by A5, XBOOLE_0:def_10; ::_thesis: verum
end;
supposeA10: k >= n ; ::_thesis: A |^ (m,n) = (A |^ (m,k)) \/ (A |^ ((k + 1),n))
then  k + 1 > n + 0 by XREAL_1:8;
then  A |^ ((k + 1),n) = {} by Th21;
hence  A |^ (m,n) = (A |^ (m,k)) \/ (A |^ ((k + 1),n)) by A2, A10, XXREAL_0:1; ::_thesis: verum
end;
end;
end;

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))
proof
let E be set ; ::_thesis: 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))
let A be Subset of (E ^omega); ::_thesis: for m, n being Nat st m <= n + 1 holds
A |^ (m,(n + 1)) = (A |^ (m,n)) \/ (A |^ (n + 1))
let m, n be Nat; ::_thesis: ( m <= n + 1 implies A |^ (m,(n + 1)) = (A |^ (m,n)) \/ (A |^ (n + 1)) )
assume A1: m <= n + 1 ; ::_thesis: A |^ (m,(n + 1)) = (A |^ (m,n)) \/ (A |^ (n + 1))
percases ( m <= n or m = n + 1 ) by A1, NAT_1:8;
supposeA2: m <= n ; ::_thesis: A |^ (m,(n + 1)) = (A |^ (m,n)) \/ (A |^ (n + 1))
 n < n + 1 by NAT_1:13;
then  A |^ (m,(n + 1)) = (A |^ (m,n)) \/ (A |^ ((n + 1),(n + 1))) by A2, Th25;
hence  A |^ (m,(n + 1)) = (A |^ (m,n)) \/ (A |^ (n + 1)) by Th22; ::_thesis: verum
end;
supposeA3: m = n + 1 ; ::_thesis: A |^ (m,(n + 1)) = (A |^ (m,n)) \/ (A |^ (n + 1))
then A4: m > n by NAT_1:13;
thus A |^ (m,(n + 1)) = {} \/ (A |^ (n + 1)) by A3, Th22
.= (A |^ (m,n)) \/ (A |^ (n + 1)) by A4, Th21 ; ::_thesis: verum
end;
end;
end;

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))
proof
let E be set ; ::_thesis: 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))
let A be Subset of (E ^omega); ::_thesis: for m, n being Nat st m <= n holds
A |^ (m,n) = (A |^ m) \/ (A |^ ((m + 1),n))
let m, n be Nat; ::_thesis: ( m <= n implies A |^ (m,n) = (A |^ m) \/ (A |^ ((m + 1),n)) )
assume A1: m <= n ; ::_thesis: A |^ (m,n) = (A |^ m) \/ (A |^ ((m + 1),n))
percases ( m < n or m = n ) by A1, XXREAL_0:1;
suppose m < n ; ::_thesis: A |^ (m,n) = (A |^ m) \/ (A |^ ((m + 1),n))
then  A |^ (m,n) = (A |^ (m,m)) \/ (A |^ ((m + 1),n)) by Th25;
hence  A |^ (m,n) = (A |^ m) \/ (A |^ ((m + 1),n)) by Th22; ::_thesis: verum
end;
supposeA2: m = n ; ::_thesis: A |^ (m,n) = (A |^ m) \/ (A |^ ((m + 1),n))
then A3: m + 1 > n by NAT_1:13;
thus A |^ (m,n) = (A |^ m) \/ {} by A2, Th22
.= (A |^ m) \/ (A |^ ((m + 1),n)) by A3, Th21 ; ::_thesis: verum
end;
end;
end;

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))
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for n being Nat holds A |^ (n,(n + 1)) = (A |^ n) \/ (A |^ (n + 1))
let A be Subset of (E ^omega); ::_thesis: for n being Nat holds A |^ (n,(n + 1)) = (A |^ n) \/ (A |^ (n + 1))
let n be Nat; ::_thesis: A |^ (n,(n + 1)) = (A |^ n) \/ (A |^ (n + 1))
thus A |^ (n,(n + 1)) = (A |^ (n,n)) \/ (A |^ (n + 1)) by Th26, NAT_1:11
.= (A |^ n) \/ (A |^ (n + 1)) by Th22 ; ::_thesis: verum
end;

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)
proof
let E be set ; ::_thesis: 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)
let A, B be Subset of (E ^omega); ::_thesis: for m, n being Nat st A c= B holds
A |^ (m,n) c= B |^ (m,n)
let m, n be Nat; ::_thesis: ( A c= B implies A |^ (m,n) c= B |^ (m,n) )
assume A1: A c= B ; ::_thesis: A |^ (m,n) c= B |^ (m,n)
thus  A |^ (m,n) c= B |^ (m,n) ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A |^ (m,n) or x in B |^ (m,n) )
assume  x in A |^ (m,n) ; ::_thesis: x in B |^ (m,n)
then consider k being Nat such that
A2: ( m <= k & k <= n & x in A |^ k ) by Th19;
 A |^ k c= B |^ k by A1, FLANG_1:37;
hence  x in B |^ (m,n) by A2, Th19; ::_thesis: verum
end;
end;

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 & x <> <%> E & ( m > 0 or n > 0 ) holds
A |^ (m,n) <> {(<%> E)}
proof
let x, E be set ; ::_thesis: for A being Subset of (E ^omega)
for m, n being Nat st x in A & x <> <%> E & ( m > 0 or n > 0 ) holds
A |^ (m,n) <> {(<%> E)}
let A be Subset of (E ^omega); ::_thesis: for m, n being Nat st x in A & x <> <%> E & ( m > 0 or n > 0 ) holds
A |^ (m,n) <> {(<%> E)}
let m, n be Nat; ::_thesis: ( x in A & x <> <%> E & ( m > 0 or n > 0 ) implies A |^ (m,n) <> {(<%> E)} )
assume that
A1: x in A and
A2: x <> <%> E and
A3: ( m > 0 or n > 0 ) ; ::_thesis: A |^ (m,n) <> {(<%> E)}
percases ( m > n or ( m <= n & m > 0 ) or ( m <= n & n > 0 ) ) by A3;
suppose m > n ; ::_thesis: A |^ (m,n) <> {(<%> E)}
hence  A |^ (m,n) <> {(<%> E)} by Th21; ::_thesis: verum
end;
supposeA4: ( m <= n & m > 0 ) ; ::_thesis: A |^ (m,n) <> {(<%> E)}
A5: A |^ m <> {} by A1, FLANG_1:27;
 A |^ m <> {(<%> E)} by A1, A2, A4, Th7;
then A6: ex x being set st
( x in A |^ m & x <> <%> E ) by A5, ZFMISC_1:35;
 A |^ m c= A |^ (m,n) by A4, Th20;
hence  A |^ (m,n) <> {(<%> E)} by A6, TARSKI:def_1; ::_thesis: verum
end;
supposeA7: ( m <= n & n > 0 ) ; ::_thesis: A |^ (m,n) <> {(<%> E)}
A8: A |^ n <> {} by A1, FLANG_1:27;
 A |^ n <> {(<%> E)} by A1, A2, A7, Th7;
then A9: ex x being set st
( x in A |^ n & x <> <%> E ) by A8, ZFMISC_1:35;
 A |^ n c= A |^ (m,n) by A7, Th20;
hence  A |^ (m,n) <> {(<%> E)} by A9, TARSKI:def_1; ::_thesis: verum
end;
end;
end;

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 & A = {(<%> E)} ) or ( m = 0 & n = 0 ) or ( m = 0 & A = {} ) ) )
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for m, n being Nat holds
( A |^ (m,n) = {(<%> E)} iff ( ( m <= n & A = {(<%> E)} ) or ( m = 0 & n = 0 ) or ( m = 0 & A = {} ) ) )
let A be Subset of (E ^omega); ::_thesis: for m, n being Nat holds
( A |^ (m,n) = {(<%> E)} iff ( ( m <= n & A = {(<%> E)} ) or ( m = 0 & n = 0 ) or ( m = 0 & A = {} ) ) )
let m, n be Nat; ::_thesis: ( A |^ (m,n) = {(<%> E)} iff ( ( m <= n & A = {(<%> E)} ) or ( m = 0 & n = 0 ) or ( m = 0 & A = {} ) ) )
thus  ( not A |^ (m,n) = {(<%> E)} or ( m <= n & A = {(<%> E)} ) or ( m = 0 & n = 0 ) or ( m = 0 & A = {} ) ) ::_thesis: ( ( ( m <= n & A = {(<%> E)} ) or ( m = 0 & n = 0 ) or ( m = 0 & A = {} ) ) implies A |^ (m,n) = {(<%> E)} )
proof
assume that
A1: A |^ (m,n) = {(<%> E)} and
A2: ( ( m > n or A <> {(<%> E)} ) & ( m <> 0 or n <> 0 ) & ( m <> 0 or A <> {} ) ) ; ::_thesis: contradiction
percases ( m > n or ( m <= n & A <> {(<%> E)} & ( m <> 0 or ( n <> 0 & A <> {} ) ) ) ) by A2;
suppose m > n ; ::_thesis: contradiction
hence  contradiction by A1, Th21; ::_thesis: verum
end;
supposeA3: ( m <= n & A <> {(<%> E)} & ( m <> 0 or ( n <> 0 & A <> {} ) ) ) ; ::_thesis: contradiction
percases ( m <> 0 or ( n <> 0 & A <> {} ) ) by A3;
supposeA4: m <> 0 ; ::_thesis: contradiction
percases ( A = {} or A <> {} ) ;
suppose A = {} ; ::_thesis: contradiction
hence  contradiction by A1, A4, Th21; ::_thesis: verum
end;
suppose A <> {} ; ::_thesis: contradiction
then  ex x being set st
( x in A & x <> <%> E ) by A3, ZFMISC_1:35;
hence  contradiction by A1, A4, Th30; ::_thesis: verum
end;
end;
end;
supposeA5: ( n <> 0 & A <> {} ) ; ::_thesis: contradiction
then  ex x being set st
( x in A & x <> <%> E ) by A3, ZFMISC_1:35;
hence  contradiction by A1, A5, Th30; ::_thesis: verum
end;
end;
end;
end;
end;
assume A6: ( ( m <= n & A = {(<%> E)} ) or ( m = 0 & n = 0 ) or ( m = 0 & A = {} ) ) ; ::_thesis: A |^ (m,n) = {(<%> E)}
percases ( ( m <= n & A = {(<%> E)} ) or ( m = 0 & n = 0 ) or ( m = 0 & A = {} ) ) by A6;
supposeA7: ( m <= n & A = {(<%> E)} ) ; ::_thesis: A |^ (m,n) = {(<%> E)}
A8: now__::_thesis:_for_x_being_set_st_x_in_{(<%>_E)}_holds_
x_in_A_|^_(m,n)
let x be set ; ::_thesis: ( x in {(<%> E)} implies x in A |^ (m,n) )
assume  x in {(<%> E)} ; ::_thesis: x in A |^ (m,n)
then A9: x in {(<%> E)} |^ m by FLANG_1:29;
 {(<%> E)} |^ m c= {(<%> E)} |^ (m,n) by A7, Th20;
hence  x in A |^ (m,n) by A7, A9; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_A_|^_(m,n)_holds_
x_in_{(<%>_E)}
let x be set ; ::_thesis: ( x in A |^ (m,n) implies x in {(<%> E)} )
assume  x in A |^ (m,n) ; ::_thesis: x in {(<%> E)}
then  ex k being Nat st
( m <= k & k <= n & x in {(<%> E)} |^ k ) by A7, Th19;
hence  x in {(<%> E)} by FLANG_1:29; ::_thesis: verum
end;
hence  A |^ (m,n) = {(<%> E)} by A8, TARSKI:1; ::_thesis: verum
end;
supposeA10: ( m = 0 & n = 0 ) ; ::_thesis: A |^ (m,n) = {(<%> E)}
A |^ (0,0) = A |^ 0 by Th22
.= {(<%> E)} by FLANG_1:29 ;
hence  A |^ (m,n) = {(<%> E)} by A10; ::_thesis: verum
end;
supposeA11: ( m = 0 & A = {} ) ; ::_thesis: A |^ (m,n) = {(<%> E)}
now__::_thesis:_for_x_being_set_holds_not_x_in_A_|^_(1,n)
let x be set ; ::_thesis: not x in A |^ (1,n)
assume  x in A |^ (1,n) ; ::_thesis: contradiction
then  ex k being Nat st
( 1 <= k & k <= n & x in A |^ k ) by Th19;
hence  contradiction by A11, FLANG_1:27; ::_thesis: verum
end;
then A12: A |^ (1,n) = {} by XBOOLE_0:def_1;
A |^ (0,n) = (A |^ (0,0)) \/ (A |^ ((0 + 1),n)) by Th25
.= (A |^ 0) \/ (A |^ ((0 + 1),n)) by Th22
.= {(<%> E)} by A12, FLANG_1:29 ;
hence  A |^ (m,n) = {(<%> E)} by A11; ::_thesis: verum
end;
end;
end;

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 *
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for m, n being Nat holds A |^ (m,n) c= A *
let A be Subset of (E ^omega); ::_thesis: for m, n being Nat holds A |^ (m,n) c= A *
let m, n be Nat; ::_thesis: A |^ (m,n) c= A *
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A |^ (m,n) or x in A * )
assume  x in A |^ (m,n) ; ::_thesis: x in A *
then  ex k being Nat st
( m <= k & k <= n & x in A |^ k ) by Th19;
hence  x in A * by FLANG_1:41; ::_thesis: verum
end;

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 & <%> E in A ) ) )
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for m, n being Nat holds
( <%> E in A |^ (m,n) iff ( m = 0 or ( m <= n & <%> E in A ) ) )
let A be Subset of (E ^omega); ::_thesis: for m, n being Nat holds
( <%> E in A |^ (m,n) iff ( m = 0 or ( m <= n & <%> E in A ) ) )
let m, n be Nat; ::_thesis: ( <%> E in A |^ (m,n) iff ( m = 0 or ( m <= n & <%> E in A ) ) )
thus  ( not <%> E in A |^ (m,n) or m = 0 or ( m <= n & <%> E in A ) ) ::_thesis: ( ( m = 0 or ( m <= n & <%> E in A ) ) implies <%> E in A |^ (m,n) )
proof
assume that
A1: <%> E in A |^ (m,n) and
A2: ( m <> 0 & ( m > n or not <%> E in A ) ) ; ::_thesis: contradiction
percases ( ( m <> 0 & m > n ) or ( m <> 0 & not <%> E in A ) ) by A2;
suppose ( m <> 0 & m > n ) ; ::_thesis: contradiction
hence  contradiction by A1, Th21; ::_thesis: verum
end;
supposeA3: ( m <> 0 & not <%> E in A ) ; ::_thesis: contradiction
consider k being Nat such that
A4: m <= k and
 k <= n and
A5: <%> E in A |^ k by A1, Th19;
 k > 0 by A3, A4;
hence  contradiction by A3, A5, FLANG_1:31; ::_thesis: verum
end;
end;
end;
assume A6: ( m = 0 or ( m <= n & <%> E in A ) ) ; ::_thesis: <%> E in A |^ (m,n)
percases ( m = 0 or ( m <= n & <%> E in A ) ) by A6;
supposeA7: m = 0 ; ::_thesis: <%> E in A |^ (m,n)
 {(<%> E)} = A |^ 0 by FLANG_1:29;
then A8: {(<%> E)} c= A |^ (0,n) by Th20;
 <%> E in {(<%> E)} by TARSKI:def_1;
hence  <%> E in A |^ (m,n) by A7, A8; ::_thesis: verum
end;
suppose ( m <= n & <%> E in A ) ; ::_thesis: <%> E in A |^ (m,n)
then  ( <%> E in A |^ m & A |^ m c= A |^ (m,n) ) by Th20, FLANG_1:30;
hence  <%> E in A |^ (m,n) ; ::_thesis: verum
end;
end;
end;

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 & m <= n holds
A |^ (m,n) = A |^ n
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for m, n being Nat st <%> E in A & m <= n holds
A |^ (m,n) = A |^ n
let A be Subset of (E ^omega); ::_thesis: for m, n being Nat st <%> E in A & m <= n holds
A |^ (m,n) = A |^ n
let m, n be Nat; ::_thesis: ( <%> E in A & m <= n implies A |^ (m,n) = A |^ n )
assume that
A1: <%> E in A and
A2: m <= n ; ::_thesis: A |^ (m,n) = A |^ n
A3: A |^ (m,n) c= A |^ n
proof
A4: now__::_thesis:_for_k_being_Nat_st_k_<=_n_holds_
A_|^_k_c=_A_|^_n
let k be Nat; ::_thesis: ( k <= n implies A |^ b1 c= A |^ n )
assume A5: k <= n ; ::_thesis: A |^ b1 c= A |^ n
percases ( k < n or k = n ) by A5, XXREAL_0:1;
suppose k < n ; ::_thesis: A |^ b1 c= A |^ n
hence  A |^ k c= A |^ n by A1, FLANG_1:36; ::_thesis: verum
end;
suppose k = n ; ::_thesis: A |^ b1 c= A |^ n
hence  A |^ k c= A |^ n ; ::_thesis: verum
end;
end;
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A |^ (m,n) or x in A |^ n )
assume  x in A |^ (m,n) ; ::_thesis: x in A |^ n
then consider k being Nat such that
 m <= k and
A6: k <= n and
A7: x in A |^ k by Th19;
 A |^ k c= A |^ n by A4, A6;
hence  x in A |^ n by A7; ::_thesis: verum
end;
 A |^ n c= A |^ (m,n) by A2, Th20;
hence  A |^ (m,n) = A |^ n by A3, XBOOLE_0:def_10; ::_thesis: verum
end;

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))
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for m, n, k being Nat holds (A |^ (m,n)) ^^ (A |^ k) = (A |^ k) ^^ (A |^ (m,n))
let A be Subset of (E ^omega); ::_thesis: for m, n, k being Nat holds (A |^ (m,n)) ^^ (A |^ k) = (A |^ k) ^^ (A |^ (m,n))
let m, n, k be Nat; ::_thesis: (A |^ (m,n)) ^^ (A |^ k) = (A |^ k) ^^ (A |^ (m,n))
A1: now__::_thesis:_for_x_being_set_st_x_in_(A_|^_k)_^^_(A_|^_(m,n))_holds_
x_in_(A_|^_(m,n))_^^_(A_|^_k)
let x be set ; ::_thesis: ( x in (A |^ k) ^^ (A |^ (m,n)) implies x in (A |^ (m,n)) ^^ (A |^ k) )
assume  x in (A |^ k) ^^ (A |^ (m,n)) ; ::_thesis: x in (A |^ (m,n)) ^^ (A |^ k)
then consider a, b being Element of E ^omega  such that
A2: a in A |^ k and
A3: b in A |^ (m,n) and
A4: x = a ^ b by FLANG_1:def_1;
consider mn being Nat such that
A5: ( m <= mn & mn <= n ) and
A6: b in A |^ mn by A3, Th19;
 A |^ mn c= A |^ (m,n) by A5, Th20;
then A7: (A |^ mn) ^^ (A |^ k) c= (A |^ (m,n)) ^^ (A |^ k) by FLANG_1:17;
 a ^ b in (A |^ k) ^^ (A |^ mn) by A2, A6, FLANG_1:def_1;
then  a ^ b in (A |^ mn) ^^ (A |^ k) by Th12;
hence  x in (A |^ (m,n)) ^^ (A |^ k) by A4, A7; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_(A_|^_(m,n))_^^_(A_|^_k)_holds_
x_in_(A_|^_k)_^^_(A_|^_(m,n))
let x be set ; ::_thesis: ( x in (A |^ (m,n)) ^^ (A |^ k) implies x in (A |^ k) ^^ (A |^ (m,n)) )
assume  x in (A |^ (m,n)) ^^ (A |^ k) ; ::_thesis: x in (A |^ k) ^^ (A |^ (m,n))
then consider a, b being Element of E ^omega  such that
A8: a in A |^ (m,n) and
A9: b in A |^ k and
A10: x = a ^ b by FLANG_1:def_1;
consider mn being Nat such that
A11: ( m <= mn & mn <= n ) and
A12: a in A |^ mn by A8, Th19;
 A |^ mn c= A |^ (m,n) by A11, Th20;
then A13: (A |^ k) ^^ (A |^ mn) c= (A |^ k) ^^ (A |^ (m,n)) by FLANG_1:17;
 a ^ b in (A |^ mn) ^^ (A |^ k) by A9, A12, FLANG_1:def_1;
then  a ^ b in (A |^ k) ^^ (A |^ mn) by Th12;
hence  x in (A |^ k) ^^ (A |^ (m,n)) by A10, A13; ::_thesis: verum
end;
hence  (A |^ (m,n)) ^^ (A |^ k) = (A |^ k) ^^ (A |^ (m,n)) by A1, TARSKI:1; ::_thesis: verum
end;

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))
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for m, n being Nat holds (A |^ (m,n)) ^^ A = A ^^ (A |^ (m,n))
let A be Subset of (E ^omega); ::_thesis: for m, n being Nat holds (A |^ (m,n)) ^^ A = A ^^ (A |^ (m,n))
let m, n be Nat; ::_thesis: (A |^ (m,n)) ^^ A = A ^^ (A |^ (m,n))
thus (A |^ (m,n)) ^^ A = (A |^ (m,n)) ^^ (A |^ 1) by FLANG_1:25
.= (A |^ 1) ^^ (A |^ (m,n)) by Th35
.= A ^^ (A |^ (m,n)) by FLANG_1:25 ; ::_thesis: verum
end;

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 & k <= l holds
(A |^ (m,n)) ^^ (A |^ (k,l)) = A |^ ((m + k),(n + l))
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for m, n, k, l being Nat st m <= n & k <= l holds
(A |^ (m,n)) ^^ (A |^ (k,l)) = A |^ ((m + k),(n + l))
let A be Subset of (E ^omega); ::_thesis: for m, n, k, l being Nat st m <= n & k <= l holds
(A |^ (m,n)) ^^ (A |^ (k,l)) = A |^ ((m + k),(n + l))
let m, n, k, l be Nat; ::_thesis: ( m <= n & k <= l implies (A |^ (m,n)) ^^ (A |^ (k,l)) = A |^ ((m + k),(n + l)) )
assume A1: ( m <= n & k <= l ) ; ::_thesis: (A |^ (m,n)) ^^ (A |^ (k,l)) = A |^ ((m + k),(n + l))
A2: now__::_thesis:_for_x_being_set_st_x_in_A_|^_((m_+_k),(n_+_l))_holds_
x_in_(A_|^_(m,n))_^^_(A_|^_(k,l))
let x be set ; ::_thesis: ( x in A |^ ((m + k),(n + l)) implies x in (A |^ (m,n)) ^^ (A |^ (k,l)) )
assume  x in A |^ ((m + k),(n + l)) ; ::_thesis: x in (A |^ (m,n)) ^^ (A |^ (k,l))
then consider i being Nat such that
A3: ( m + k <= i & i <= n + l ) and
A4: x in A |^ i by Th19;
consider mn, kl being Nat such that
A5: mn + kl = i and
A6: ( m <= mn & mn <= n & k <= kl & kl <= l ) by A1, A3, Th2;
 ( A |^ mn c= A |^ (m,n) & A |^ kl c= A |^ (k,l) ) by A6, Th20;
then  (A |^ mn) ^^ (A |^ kl) c= (A |^ (m,n)) ^^ (A |^ (k,l)) by FLANG_1:17;
then  A |^ (mn + kl) c= (A |^ (m,n)) ^^ (A |^ (k,l)) by FLANG_1:33;
hence  x in (A |^ (m,n)) ^^ (A |^ (k,l)) by A4, A5; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_(A_|^_(m,n))_^^_(A_|^_(k,l))_holds_
x_in_A_|^_((m_+_k),(n_+_l))
let x be set ; ::_thesis: ( x in (A |^ (m,n)) ^^ (A |^ (k,l)) implies x in A |^ ((m + k),(n + l)) )
assume  x in (A |^ (m,n)) ^^ (A |^ (k,l)) ; ::_thesis: x in A |^ ((m + k),(n + l))
then consider a, b being Element of E ^omega  such that
A7: a in A |^ (m,n) and
A8: b in A |^ (k,l) and
A9: x = a ^ b by FLANG_1:def_1;
consider kl being Nat such that
A10: k <= kl and
A11: kl <= l and
A12: b in A |^ kl by A8, Th19;
consider mn being Nat such that
A13: m <= mn and
A14: mn <= n and
A15: a in A |^ mn by A7, Th19;
A16: mn + kl <= n + l by A14, A11, XREAL_1:7;
 ( a ^ b in A |^ (mn + kl) & m + k <= mn + kl ) by A13, A15, A10, A12, FLANG_1:40, XREAL_1:7;
hence  x in A |^ ((m + k),(n + l)) by A9, A16, Th19; ::_thesis: verum
end;
hence  (A |^ (m,n)) ^^ (A |^ (k,l)) = A |^ ((m + k),(n + l)) by A2, TARSKI:1; ::_thesis: verum
end;

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
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for m, n being Nat holds A |^ ((m + 1),(n + 1)) = (A |^ (m,n)) ^^ A
let A be Subset of (E ^omega); ::_thesis: for m, n being Nat holds A |^ ((m + 1),(n + 1)) = (A |^ (m,n)) ^^ A
let m, n be Nat; ::_thesis: A |^ ((m + 1),(n + 1)) = (A |^ (m,n)) ^^ A
percases ( m <= n or m > n ) ;
suppose m <= n ; ::_thesis: A |^ ((m + 1),(n + 1)) = (A |^ (m,n)) ^^ A
hence A |^ ((m + 1),(n + 1)) = (A |^ (m,n)) ^^ (A |^ (1,1)) by Th37
.= (A |^ (m,n)) ^^ (A |^ 1) by Th22
.= (A |^ (m,n)) ^^ A by FLANG_1:25 ;
::_thesis: verum
end;
supposeA1: m > n ; ::_thesis: A |^ ((m + 1),(n + 1)) = (A |^ (m,n)) ^^ A
then  A |^ (m,n) = {} by Th21;
then A2: (A |^ (m,n)) ^^ A = {} by FLANG_1:12;
 m + 1 > n + 1 by A1, XREAL_1:8;
hence  A |^ ((m + 1),(n + 1)) = (A |^ (m,n)) ^^ A by A2, Th21; ::_thesis: verum
end;
end;
end;

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))
proof
let E be set ; ::_thesis: 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))
let A be Subset of (E ^omega); ::_thesis: for m, n, k, l being Nat holds (A |^ (m,n)) ^^ (A |^ (k,l)) = (A |^ (k,l)) ^^ (A |^ (m,n))
let m, n, k, l be Nat; ::_thesis: (A |^ (m,n)) ^^ (A |^ (k,l)) = (A |^ (k,l)) ^^ (A |^ (m,n))
percases ( ( m <= n & k <= l ) or m > n or k > l ) ;
supposeA1: ( m <= n & k <= l ) ; ::_thesis: (A |^ (m,n)) ^^ (A |^ (k,l)) = (A |^ (k,l)) ^^ (A |^ (m,n))
hence (A |^ (m,n)) ^^ (A |^ (k,l)) = A |^ ((m + k),(n + l)) by Th37
.= (A |^ (k,l)) ^^ (A |^ (m,n)) by A1, Th37 ;
::_thesis: verum
end;
suppose m > n ; ::_thesis: (A |^ (m,n)) ^^ (A |^ (k,l)) = (A |^ (k,l)) ^^ (A |^ (m,n))
then A2: A |^ (m,n) = {} by Th21;
then  (A |^ (m,n)) ^^ (A |^ (k,l)) = {} by FLANG_1:12;
hence  (A |^ (m,n)) ^^ (A |^ (k,l)) = (A |^ (k,l)) ^^ (A |^ (m,n)) by A2, FLANG_1:12; ::_thesis: verum
end;
suppose k > l ; ::_thesis: (A |^ (m,n)) ^^ (A |^ (k,l)) = (A |^ (k,l)) ^^ (A |^ (m,n))
then A3: A |^ (k,l) = {} by Th21;
then  (A |^ (m,n)) ^^ (A |^ (k,l)) = {} by FLANG_1:12;
hence  (A |^ (m,n)) ^^ (A |^ (k,l)) = (A |^ (k,l)) ^^ (A |^ (m,n)) by A3, FLANG_1:12; ::_thesis: verum
end;
end;
end;

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))
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for m, n, k being Nat holds (A |^ (m,n)) |^ k = A |^ ((m * k),(n * k))
let A be Subset of (E ^omega); ::_thesis: for m, n, k being Nat holds (A |^ (m,n)) |^ k = A |^ ((m * k),(n * k))
let m, n, k be Nat; ::_thesis: (A |^ (m,n)) |^ k = A |^ ((m * k),(n * k))
percases ( m <= n or k = 0 or ( m > n & k <> 0 ) ) ;
supposeA1: m <= n ; ::_thesis: (A |^ (m,n)) |^ k = A |^ ((m * k),(n * k))
defpred S1[ Nat] means (A |^ (m,n)) |^ $1 = A |^ ((m * $1),(n * $1));
A2: now__::_thesis:_for_k_being_Nat_st_S1[k]_holds_
S1[k_+_1]
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
A3: m * k <= n * k by A1, XREAL_1:64;
assume  S1[k] ; ::_thesis: S1[k + 1]
then (A |^ (m,n)) |^ (k + 1) = (A |^ ((m * k),(n * k))) ^^ (A |^ (m,n)) by FLANG_1:23
.= A |^ (((m * k) + m),((n * k) + n)) by A1, A3, Th37
.= A |^ ((m * (k + 1)),(n * (k + 1))) ;
hence  S1[k + 1] ; ::_thesis: verum
end;
(A |^ (m,n)) |^ 0 = {(<%> E)} by FLANG_1:24
.= A |^ 0 by FLANG_1:24
.= A |^ ((m * 0),(n * 0)) by Th22 ;
then A4: S1[ 0 ] ;
 for k being Nat holds S1[k] from NAT_1:sch_2(A4, A2);
hence  (A |^ (m,n)) |^ k = A |^ ((m * k),(n * k)) ; ::_thesis: verum
end;
supposeA5: k = 0 ; ::_thesis: (A |^ (m,n)) |^ k = A |^ ((m * k),(n * k))
hence (A |^ (m,n)) |^ k = {(<%> E)} by FLANG_1:24
.= A |^ 0 by FLANG_1:24
.= A |^ ((m * k),(n * k)) by A5, Th22 ;
::_thesis: verum
end;
supposeA6: ( m > n & k <> 0 ) ; ::_thesis: (A |^ (m,n)) |^ k = A |^ ((m * k),(n * k))
then  A |^ (m,n) = {} by Th21;
then A7: (A |^ (m,n)) |^ k = {} by A6, FLANG_1:27;
 m * k > n * k by A6, XREAL_1:68;
hence  (A |^ (m,n)) |^ k = A |^ ((m * k),(n * k)) by A7, Th21; ::_thesis: verum
end;
end;
end;

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))
proof
let E be set ; ::_thesis: 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))
let A be Subset of (E ^omega); ::_thesis: for k, m, n being Nat holds (A |^ (k + 1)) |^ (m,n) c= ((A |^ k) |^ (m,n)) ^^ (A |^ (m,n))
let k, m, n be Nat; ::_thesis: (A |^ (k + 1)) |^ (m,n) c= ((A |^ k) |^ (m,n)) ^^ (A |^ (m,n))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A |^ (k + 1)) |^ (m,n) or x in ((A |^ k) |^ (m,n)) ^^ (A |^ (m,n)) )
assume  x in (A |^ (k + 1)) |^ (m,n) ; ::_thesis: x in ((A |^ k) |^ (m,n)) ^^ (A |^ (m,n))
then consider mn being Nat such that
A1: ( m <= mn & mn <= n ) and
A2: x in (A |^ (k + 1)) |^ mn by Th19;
 A |^ mn c= A |^ (m,n) by A1, Th20;
then A3: ((A |^ k) |^ (m,n)) ^^ (A |^ mn) c= ((A |^ k) |^ (m,n)) ^^ (A |^ (m,n)) by FLANG_1:17;
 x in A |^ ((k + 1) * mn) by A2, FLANG_1:34;
then  x in A |^ ((k * mn) + mn) ;
then  x in (A |^ (k * mn)) ^^ (A |^ mn) by FLANG_1:33;
then A4: x in ((A |^ k) |^ mn) ^^ (A |^ mn) by FLANG_1:34;
 (A |^ k) |^ mn c= (A |^ k) |^ (m,n) by A1, Th20;
then  ((A |^ k) |^ mn) ^^ (A |^ mn) c= ((A |^ k) |^ (m,n)) ^^ (A |^ mn) by FLANG_1:17;
then  x in ((A |^ k) |^ (m,n)) ^^ (A |^ mn) by A4;
hence  x in ((A |^ k) |^ (m,n)) ^^ (A |^ (m,n)) by A3; ::_thesis: verum
end;

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))
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for k, m, n being Nat holds (A |^ k) |^ (m,n) c= A |^ ((k * m),(k * n))
let A be Subset of (E ^omega); ::_thesis: for k, m, n being Nat holds (A |^ k) |^ (m,n) c= A |^ ((k * m),(k * n))
let k, m, n be Nat; ::_thesis: (A |^ k) |^ (m,n) c= A |^ ((k * m),(k * n))
percases ( m <= n or m > n ) ;
supposeA1: m <= n ; ::_thesis: (A |^ k) |^ (m,n) c= A |^ ((k * m),(k * n))
defpred S1[ Nat] means (A |^ $1) |^ (m,n) c= A |^ (($1 * m),($1 * n));
A2: now__::_thesis:_for_l_being_Nat_st_S1[l]_holds_
S1[l_+_1]
let l be Nat; ::_thesis: ( S1[l] implies S1[l + 1] )
A3: l * m <= l * n by A1, XREAL_1:64;
assume  S1[l] ; ::_thesis: S1[l + 1]
then A4: ((A |^ l) |^ (m,n)) ^^ ((A |^ 1) |^ (m,n)) c= (A |^ ((l * m),(l * n))) ^^ ((A |^ 1) |^ (m,n)) by FLANG_1:17;
 (A |^ (l + 1)) |^ (m,n) c= ((A |^ l) |^ (m,n)) ^^ (A |^ (m,n)) by Th41;
then A5: (A |^ (l + 1)) |^ (m,n) c= ((A |^ l) |^ (m,n)) ^^ ((A |^ 1) |^ (m,n)) by FLANG_1:25;
(A |^ ((l * m),(l * n))) ^^ ((A |^ 1) |^ (m,n)) = (A |^ ((l * m),(l * n))) ^^ (A |^ (m,n)) by FLANG_1:25
.= A |^ (((l * m) + m),((l * n) + n)) by A1, A3, Th37
.= A |^ (((l + 1) * m),((l + 1) * n)) ;
hence  S1[l + 1] by A5, A4, XBOOLE_1:1; ::_thesis: verum
end;
(A |^ 0) |^ (m,n) = {(<%> E)} |^ (m,n) by FLANG_1:24
.= {(<%> E)} by A1, Th31
.= A |^ 0 by FLANG_1:24
.= A |^ ((0 * m),(0 * n)) by Th22 ;
then A6: S1[ 0 ] ;
 for l being Nat holds S1[l] from NAT_1:sch_2(A6, A2);
hence  (A |^ k) |^ (m,n) c= A |^ ((k * m),(k * n)) ; ::_thesis: verum
end;
suppose m > n ; ::_thesis: (A |^ k) |^ (m,n) c= A |^ ((k * m),(k * n))
then  (A |^ k) |^ (m,n) = {} by Th21;
hence  (A |^ k) |^ (m,n) c= A |^ ((k * m),(k * n)) by XBOOLE_1:2; ::_thesis: verum
end;
end;
end;

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
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for k, m, n being Nat holds (A |^ k) |^ (m,n) c= (A |^ (m,n)) |^ k
let A be Subset of (E ^omega); ::_thesis: for k, m, n being Nat holds (A |^ k) |^ (m,n) c= (A |^ (m,n)) |^ k
let k, m, n be Nat; ::_thesis: (A |^ k) |^ (m,n) c= (A |^ (m,n)) |^ k
 (A |^ (m,n)) |^ k = A |^ ((m * k),(n * k)) by Th40;
hence  (A |^ k) |^ (m,n) c= (A |^ (m,n)) |^ k by Th42; ::_thesis: verum
end;

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))
proof
let E be set ; ::_thesis: 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))
let A be Subset of (E ^omega); ::_thesis: for k, l, m, n being Nat holds (A |^ (k + l)) |^ (m,n) c= ((A |^ k) |^ (m,n)) ^^ ((A |^ l) |^ (m,n))
let k, l, m, n be Nat; ::_thesis: (A |^ (k + l)) |^ (m,n) c= ((A |^ k) |^ (m,n)) ^^ ((A |^ l) |^ (m,n))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A |^ (k + l)) |^ (m,n) or x in ((A |^ k) |^ (m,n)) ^^ ((A |^ l) |^ (m,n)) )
assume  x in (A |^ (k + l)) |^ (m,n) ; ::_thesis: x in ((A |^ k) |^ (m,n)) ^^ ((A |^ l) |^ (m,n))
then consider mn being Nat such that
A1: ( m <= mn & mn <= n ) and
A2: x in (A |^ (k + l)) |^ mn by Th19;
 x in A |^ ((k + l) * mn) by A2, FLANG_1:34;
then  x in A |^ ((k * mn) + (l * mn)) ;
then  x in (A |^ (k * mn)) ^^ (A |^ (l * mn)) by FLANG_1:33;
then consider a, b being Element of E ^omega  such that
A3: a in A |^ (k * mn) and
A4: b in A |^ (l * mn) and
A5: x = a ^ b by FLANG_1:def_1;
 b in (A |^ l) |^ mn by A4, FLANG_1:34;
then A6: b in (A |^ l) |^ (m,n) by A1, Th19;
 a in (A |^ k) |^ mn by A3, FLANG_1:34;
then  a in (A |^ k) |^ (m,n) by A1, Th19;
hence  x in ((A |^ k) |^ (m,n)) ^^ ((A |^ l) |^ (m,n)) by A5, A6, FLANG_1:def_1; ::_thesis: verum
end;

theorem Th45: :: FLANG_2:45
for E being set
for A being Subset of (E ^omega) holds A |^ (0,0) = {(<%> E)}
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds A |^ (0,0) = {(<%> E)}
let A be Subset of (E ^omega); ::_thesis: A |^ (0,0) = {(<%> E)}
thus A |^ (0,0) = A |^ 0 by Th22
.= {(<%> E)} by FLANG_1:24 ; ::_thesis: verum
end;

theorem Th46: :: FLANG_2:46
for E being set
for A being Subset of (E ^omega) holds A |^ (0,1) = {(<%> E)} \/ A
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds A |^ (0,1) = {(<%> E)} \/ A
let A be Subset of (E ^omega); ::_thesis: A |^ (0,1) = {(<%> E)} \/ A
thus A |^ (0,1) = (A |^ 0) \/ (A |^ (0 + 1)) by Th28
.= {(<%> E)} \/ (A |^ 1) by FLANG_1:24
.= {(<%> E)} \/ A by FLANG_1:25 ; ::_thesis: verum
end;

theorem :: FLANG_2:47
for E being set
for A being Subset of (E ^omega) holds A |^ (1,1) = A
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds A |^ (1,1) = A
let A be Subset of (E ^omega); ::_thesis: A |^ (1,1) = A
thus A |^ (1,1) = A |^ 1 by Th22
.= A by FLANG_1:25 ; ::_thesis: verum
end;

theorem :: FLANG_2:48
for E being set
for A being Subset of (E ^omega) holds A |^ (0,2) = ({(<%> E)} \/ A) \/ (A ^^ A)
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds A |^ (0,2) = ({(<%> E)} \/ A) \/ (A ^^ A)
let A be Subset of (E ^omega); ::_thesis: A |^ (0,2) = ({(<%> E)} \/ A) \/ (A ^^ A)
thus A |^ (0,2) = (A |^ (0,1)) \/ (A |^ (1 + 1)) by Th26
.= ({(<%> E)} \/ A) \/ (A |^ (1 + 1)) by Th46
.= ({(<%> E)} \/ A) \/ (A ^^ A) by FLANG_1:26 ; ::_thesis: verum
end;

theorem :: FLANG_2:49
for E being set
for A being Subset of (E ^omega) holds A |^ (1,2) = A \/ (A ^^ A)
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds A |^ (1,2) = A \/ (A ^^ A)
let A be Subset of (E ^omega); ::_thesis: A |^ (1,2) = A \/ (A ^^ A)
thus A |^ (1,2) = (A |^ 1) \/ (A |^ (1 + 1)) by Th28
.= A \/ (A |^ 2) by FLANG_1:25
.= A \/ (A ^^ A) by FLANG_1:26 ; ::_thesis: verum
end;

theorem :: FLANG_2:50
for E being set
for A being Subset of (E ^omega) holds A |^ (2,2) = A ^^ A
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds A |^ (2,2) = A ^^ A
let A be Subset of (E ^omega); ::_thesis: A |^ (2,2) = A ^^ A
thus A |^ (2,2) = A |^ 2 by Th22
.= A ^^ A by FLANG_1:26 ; ::_thesis: verum
end;

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 & A |^ (m,n) = {x} holds
for mn being Nat st m <= mn & mn <= n holds
A |^ mn = {x}
proof
let E, x be set ; ::_thesis: for A being Subset of (E ^omega)
for m, n being Nat st m > 0 & A |^ (m,n) = {x} holds
for mn being Nat st m <= mn & mn <= n holds
A |^ mn = {x}
let A be Subset of (E ^omega); ::_thesis: for m, n being Nat st m > 0 & A |^ (m,n) = {x} holds
for mn being Nat st m <= mn & mn <= n holds
A |^ mn = {x}
let m, n be Nat; ::_thesis: ( m > 0 & A |^ (m,n) = {x} implies for mn being Nat st m <= mn & mn <= n holds
A |^ mn = {x} )
assume that
A1: m > 0 and
A2: A |^ (m,n) = {x} ; ::_thesis: for mn being Nat st m <= mn & mn <= n holds
A |^ mn = {x}
given mn being Nat such that A3: ( m <= mn & mn <= n ) and
A4: A |^ mn <> {x} ; ::_thesis: contradiction
percases ( A |^ mn = {} or A |^ mn <> {} ) ;
supposeA5: A |^ mn = {} ; ::_thesis: contradiction
 x in A |^ (m,n) by A2, TARSKI:def_1;
then A6: ex i being Nat st
( m <= i & i <= n & x in A |^ i ) by Th19;
 A = {} by A5, FLANG_1:27;
hence  contradiction by A1, A6, FLANG_1:27; ::_thesis: verum
end;
suppose A |^ mn <> {} ; ::_thesis: contradiction
then consider y being set  such that
A7: y in A |^ mn and
A8: y <> x by A4, ZFMISC_1:35;
 y in A |^ (m,n) by A3, A7, Th19;
hence  contradiction by A2, A8, TARSKI:def_1; ::_thesis: verum
end;
end;
end;

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 & A |^ (m,n) = {x} holds
x = <%> E
proof
let x, E be set ; ::_thesis: for A being Subset of (E ^omega)
for m, n being Nat st m <> n & A |^ (m,n) = {x} holds
x = <%> E
let A be Subset of (E ^omega); ::_thesis: for m, n being Nat st m <> n & A |^ (m,n) = {x} holds
x = <%> E
let m, n be Nat; ::_thesis: ( m <> n & A |^ (m,n) = {x} implies x = <%> E )
assume that
A1: m <> n and
A2: A |^ (m,n) = {x} ; ::_thesis: x = <%> E
percases ( m > n or ( m = 0 & m <= n ) or ( m > 0 & m <= n ) ) ;
suppose m > n ; ::_thesis: x = <%> E
hence  x = <%> E by A2, Th21; ::_thesis: verum
end;
supposeA3: ( m = 0 & m <= n ) ; ::_thesis: x = <%> E
then  {(<%> E)} = A |^ m by FLANG_1:24;
then  <%> E in A |^ m by TARSKI:def_1;
then  <%> E in A |^ (m,n) by A3, Th19;
hence  x = <%> E by A2, TARSKI:def_1; ::_thesis: verum
end;
suppose ( m > 0 & m <= n ) ; ::_thesis: x = <%> E
then  ( A |^ m = {x} & A |^ n = {x} ) by A2, Th51;
hence  x = <%> E by A1, Th10; ::_thesis: verum
end;
end;
end;

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 & m <= n & ( ( <%> E in A & n > 0 ) or ( m <= 1 & 1 <= n ) ) ) )
proof
let x, E be set ; ::_thesis: for A being Subset of (E ^omega)
for m, n being Nat holds
( <%x%> in A |^ (m,n) iff ( <%x%> in A & m <= n & ( ( <%> E in A & n > 0 ) or ( m <= 1 & 1 <= n ) ) ) )
let A be Subset of (E ^omega); ::_thesis: for m, n being Nat holds
( <%x%> in A |^ (m,n) iff ( <%x%> in A & m <= n & ( ( <%> E in A & n > 0 ) or ( m <= 1 & 1 <= n ) ) ) )
let m, n be Nat; ::_thesis: ( <%x%> in A |^ (m,n) iff ( <%x%> in A & m <= n & ( ( <%> E in A & n > 0 ) or ( m <= 1 & 1 <= n ) ) ) )
thus  ( <%x%> in A |^ (m,n) implies ( <%x%> in A & m <= n & ( ( <%> E in A & n > 0 ) or ( m <= 1 & 1 <= n ) ) ) ) ::_thesis: ( <%x%> in A & m <= n & ( ( <%> E in A & n > 0 ) or ( m <= 1 & 1 <= n ) ) implies <%x%> in A |^ (m,n) )
proof
assume A1: <%x%> in A |^ (m,n) ; ::_thesis: ( <%x%> in A & m <= n & ( ( <%> E in A & n > 0 ) or ( m <= 1 & 1 <= n ) ) )
then  ex mn being Nat st
( m <= mn & mn <= n & <%x%> in A |^ mn ) by Th19;
hence  ( <%x%> in A & m <= n & ( ( <%> E in A & n > 0 ) or ( m <= 1 & 1 <= n ) ) ) by A1, Th9, Th21; ::_thesis: verum
end;
assume that
A2: <%x%> in A and
A3: m <= n and
A4: ( ( <%> E in A & n > 0 ) or ( m <= 1 & 1 <= n ) ) ; ::_thesis: <%x%> in A |^ (m,n)
percases ( ( <%> E in A & n > 0 ) or ( m <= 1 & 1 <= n ) ) by A4;
suppose ( <%> E in A & n > 0 ) ; ::_thesis: <%x%> in A |^ (m,n)
then  A c= A |^ n by FLANG_1:35;
hence  <%x%> in A |^ (m,n) by A2, A3, Th19; ::_thesis: verum
end;
supposeA5: ( m <= 1 & 1 <= n ) ; ::_thesis: <%x%> in A |^ (m,n)
 <%x%> in A |^ 1 by A2, FLANG_1:25;
hence  <%x%> in A |^ (m,n) by A5, Th19; ::_thesis: verum
end;
end;
end;

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))
proof
let E be set ; ::_thesis: 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))
let A, B be Subset of (E ^omega); ::_thesis: for m, n being Nat holds (A /\ B) |^ (m,n) c= (A |^ (m,n)) /\ (B |^ (m,n))
let m, n be Nat; ::_thesis: (A /\ B) |^ (m,n) c= (A |^ (m,n)) /\ (B |^ (m,n))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A /\ B) |^ (m,n) or x in (A |^ (m,n)) /\ (B |^ (m,n)) )
assume  x in (A /\ B) |^ (m,n) ; ::_thesis: x in (A |^ (m,n)) /\ (B |^ (m,n))
then consider mn being Nat such that
A1: ( m <= mn & mn <= n ) and
A2: x in (A /\ B) |^ mn by Th19;
A3: (A /\ B) |^ mn c= (A |^ mn) /\ (B |^ mn) by FLANG_1:39;
then  x in B |^ mn by A2, XBOOLE_0:def_4;
then A4: x in B |^ (m,n) by A1, Th19;
 x in A |^ mn by A2, A3, XBOOLE_0:def_4;
then  x in A |^ (m,n) by A1, Th19;
hence  x in (A |^ (m,n)) /\ (B |^ (m,n)) by A4, XBOOLE_0:def_4; ::_thesis: verum
end;

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)
proof
let E be set ; ::_thesis: 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)
let A, B be Subset of (E ^omega); ::_thesis: for m, n being Nat holds (A |^ (m,n)) \/ (B |^ (m,n)) c= (A \/ B) |^ (m,n)
let m, n be Nat; ::_thesis: (A |^ (m,n)) \/ (B |^ (m,n)) c= (A \/ B) |^ (m,n)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A |^ (m,n)) \/ (B |^ (m,n)) or x in (A \/ B) |^ (m,n) )
assume A1: x in (A |^ (m,n)) \/ (B |^ (m,n)) ; ::_thesis: x in (A \/ B) |^ (m,n)
percases ( x in A |^ (m,n) or x in B |^ (m,n) ) by A1, XBOOLE_0:def_3;
suppose x in A |^ (m,n) ; ::_thesis: x in (A \/ B) |^ (m,n)
then consider mn being Nat such that
A2: ( m <= mn & mn <= n ) and
A3: x in A |^ mn by Th19;
A4: (A |^ mn) \/ (B |^ mn) c= (A \/ B) |^ mn by FLANG_1:38;
 x in (A |^ mn) \/ (B |^ mn) by A3, XBOOLE_0:def_3;
hence  x in (A \/ B) |^ (m,n) by A2, A4, Th19; ::_thesis: verum
end;
suppose x in B |^ (m,n) ; ::_thesis: x in (A \/ B) |^ (m,n)
then consider mn being Nat such that
A5: ( m <= mn & mn <= n ) and
A6: x in B |^ mn by Th19;
A7: (A |^ mn) \/ (B |^ mn) c= (A \/ B) |^ mn by FLANG_1:38;
 x in (A |^ mn) \/ (B |^ mn) by A6, XBOOLE_0:def_3;
hence  x in (A \/ B) |^ (m,n) by A5, A7, Th19; ::_thesis: verum
end;
end;
end;

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))
proof
let E be set ; ::_thesis: 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))
let A be Subset of (E ^omega); ::_thesis: for m, n, k, l being Nat holds (A |^ (m,n)) |^ (k,l) c= A |^ ((m * k),(n * l))
let m, n, k, l be Nat; ::_thesis: (A |^ (m,n)) |^ (k,l) c= A |^ ((m * k),(n * l))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A |^ (m,n)) |^ (k,l) or x in A |^ ((m * k),(n * l)) )
assume  x in (A |^ (m,n)) |^ (k,l) ; ::_thesis: x in A |^ ((m * k),(n * l))
then consider kl being Nat such that
A1: ( k <= kl & kl <= l ) and
A2: x in (A |^ (m,n)) |^ kl by Th19;
 ( m * k <= m * kl & n * kl <= n * l ) by A1, NAT_1:4;
then A3: A |^ ((m * kl),(n * kl)) c= A |^ ((m * k),(n * l)) by Th23;
 x in A |^ ((m * kl),(n * kl)) by A2, Th40;
hence  x in A |^ ((m * k),(n * l)) by A3; ::_thesis: verum
end;

theorem :: FLANG_2:57
for E being set
for B, A being Subset of (E ^omega)
for m, n being Nat st m <= n & <%> E in B holds
( A c= A ^^ (B |^ (m,n)) & A c= (B |^ (m,n)) ^^ A )
proof
let E be set ; ::_thesis: for B, A being Subset of (E ^omega)
for m, n being Nat st m <= n & <%> E in B holds
( A c= A ^^ (B |^ (m,n)) & A c= (B |^ (m,n)) ^^ A )
let B, A be Subset of (E ^omega); ::_thesis: for m, n being Nat st m <= n & <%> E in B holds
( A c= A ^^ (B |^ (m,n)) & A c= (B |^ (m,n)) ^^ A )
let m, n be Nat; ::_thesis: ( m <= n & <%> E in B implies ( A c= A ^^ (B |^ (m,n)) & A c= (B |^ (m,n)) ^^ A ) )
assume  ( m <= n & <%> E in B ) ; ::_thesis: ( A c= A ^^ (B |^ (m,n)) & A c= (B |^ (m,n)) ^^ A )
then  <%> E in B |^ (m,n) by Th33;
hence  ( A c= A ^^ (B |^ (m,n)) & A c= (B |^ (m,n)) ^^ A ) by FLANG_1:16; ::_thesis: verum
end;

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 & k <= l & A c= C |^ (m,n) & B c= C |^ (k,l) holds
A ^^ B c= C |^ ((m + k),(n + l))
proof
let E be set ; ::_thesis: for A, C, B being Subset of (E ^omega)
for m, n, k, l being Nat st m <= n & k <= l & A c= C |^ (m,n) & B c= C |^ (k,l) holds
A ^^ B c= C |^ ((m + k),(n + l))
let A, C, B be Subset of (E ^omega); ::_thesis: for m, n, k, l being Nat st m <= n & k <= l & A c= C |^ (m,n) & B c= C |^ (k,l) holds
A ^^ B c= C |^ ((m + k),(n + l))
let m, n, k, l be Nat; ::_thesis: ( m <= n & k <= l & A c= C |^ (m,n) & B c= C |^ (k,l) implies A ^^ B c= C |^ ((m + k),(n + l)) )
assume that
A1: ( m <= n & k <= l ) and
A2: ( A c= C |^ (m,n) & B c= C |^ (k,l) ) ; ::_thesis: A ^^ B c= C |^ ((m + k),(n + l))
thus  A ^^ B c= C |^ ((m + k),(n + l)) ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A ^^ B or x in C |^ ((m + k),(n + l)) )
assume  x in A ^^ B ; ::_thesis: x in C |^ ((m + k),(n + l))
then consider a, b being Element of E ^omega  such that
A3: ( a in A & b in B ) and
A4: x = a ^ b by FLANG_1:def_1;
 a ^ b in (C |^ (m,n)) ^^ (C |^ (k,l)) by A2, A3, FLANG_1:def_1;
hence  x in C |^ ((m + k),(n + l)) by A1, A4, Th37; ::_thesis: verum
end;
end;

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 *
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for m, n being Nat holds (A |^ (m,n)) * c= A *
let A be Subset of (E ^omega); ::_thesis: for m, n being Nat holds (A |^ (m,n)) * c= A *
let m, n be Nat; ::_thesis: (A |^ (m,n)) * c= A *
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A |^ (m,n)) * or x in A * )
assume  x in (A |^ (m,n)) * ; ::_thesis: x in A *
then consider k being Nat such that
A1: x in (A |^ (m,n)) |^ k by FLANG_1:41;
 ( (A |^ (m,n)) |^ k = A |^ ((m * k),(n * k)) & A |^ ((m * k),(n * k)) c= A * ) by Th32, Th40;
hence  x in A * by A1; ::_thesis: verum
end;

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 *
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for m, n being Nat holds (A *) |^ (m,n) c= A *
let A be Subset of (E ^omega); ::_thesis: for m, n being Nat holds (A *) |^ (m,n) c= A *
let m, n be Nat; ::_thesis: (A *) |^ (m,n) c= A *
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A *) |^ (m,n) or x in A * )
assume  x in (A *) |^ (m,n) ; ::_thesis: x in A *
then consider mn being Nat such that
 m <= mn and
 mn <= n and
A1: x in (A *) |^ mn by Th19;
 (A *) |^ mn c= A * by FLANG_1:65;
hence  x in A * by A1; ::_thesis: verum
end;

theorem :: FLANG_2:61
for E being set
for A being Subset of (E ^omega)
for m, n being Nat st m <= n & n > 0 holds
(A *) |^ (m,n) = A *
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for m, n being Nat st m <= n & n > 0 holds
(A *) |^ (m,n) = A *
let A be Subset of (E ^omega); ::_thesis: for m, n being Nat st m <= n & n > 0 holds
(A *) |^ (m,n) = A *
let m, n be Nat; ::_thesis: ( m <= n & n > 0 implies (A *) |^ (m,n) = A * )
assume that
A1: m <= n and
A2: n > 0 ; ::_thesis: (A *) |^ (m,n) = A *
 <%> E in A * by FLANG_1:48;
hence (A *) |^ (m,n) = (A *) |^ n by A1, Th34
.= A * by A2, FLANG_1:66 ;
::_thesis: verum
end;

theorem :: FLANG_2:62
for E being set
for A being Subset of (E ^omega)
for m, n being Nat st m <= n & n > 0 & <%> E in A holds
(A |^ (m,n)) * = A *
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for m, n being Nat st m <= n & n > 0 & <%> E in A holds
(A |^ (m,n)) * = A *
let A be Subset of (E ^omega); ::_thesis: for m, n being Nat st m <= n & n > 0 & <%> E in A holds
(A |^ (m,n)) * = A *
let m, n be Nat; ::_thesis: ( m <= n & n > 0 & <%> E in A implies (A |^ (m,n)) * = A * )
assume that
A1: m <= n and
A2: n > 0 and
A3: <%> E in A ; ::_thesis: (A |^ (m,n)) * = A *
thus (A |^ (m,n)) * = (A |^ n) * by A1, A3, Th34
.= A * by A2, A3, Th16 ; ::_thesis: verum
end;

theorem :: FLANG_2:63
for E being set
for A being Subset of (E ^omega)
for m, n being Nat st m <= n & <%> E in A holds
(A |^ (m,n)) * = (A *) |^ (m,n)
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for m, n being Nat st m <= n & <%> E in A holds
(A |^ (m,n)) * = (A *) |^ (m,n)
let A be Subset of (E ^omega); ::_thesis: for m, n being Nat st m <= n & <%> E in A holds
(A |^ (m,n)) * = (A *) |^ (m,n)
let m, n be Nat; ::_thesis: ( m <= n & <%> E in A implies (A |^ (m,n)) * = (A *) |^ (m,n) )
assume that
A1: m <= n and
A2: <%> E in A ; ::_thesis: (A |^ (m,n)) * = (A *) |^ (m,n)
 ( (A |^ (m,n)) * = (A |^ n) * & (A *) |^ (m,n) = (A *) |^ n ) by A1, A2, Th34, FLANG_1:48;
hence  (A |^ (m,n)) * = (A *) |^ (m,n) by A2, Th17; ::_thesis: verum
end;

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 *
proof
let E be set ; ::_thesis: for A, B being Subset of (E ^omega)
for m, n being Nat st A c= B * holds
A |^ (m,n) c= B *
let A, B be Subset of (E ^omega); ::_thesis: for m, n being Nat st A c= B * holds
A |^ (m,n) c= B *
let m, n be Nat; ::_thesis: ( A c= B * implies A |^ (m,n) c= B * )
assume A1: A c= B * ; ::_thesis: A |^ (m,n) c= B *
thus  A |^ (m,n) c= B * ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A |^ (m,n) or x in B * )
assume  x in A |^ (m,n) ; ::_thesis: x in B *
then consider mn being Nat such that
 m <= mn and
 mn <= n and
A2: x in A |^ mn by Th19;
 A |^ mn c= B * by A1, FLANG_1:59;
hence  x in B * by A2; ::_thesis: verum
end;
end;

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))
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for m, n being Nat holds (A |^ (m,n)) ^^ (A *) = (A *) ^^ (A |^ (m,n))
let A be Subset of (E ^omega); ::_thesis: for m, n being Nat holds (A |^ (m,n)) ^^ (A *) = (A *) ^^ (A |^ (m,n))
let m, n be Nat; ::_thesis: (A |^ (m,n)) ^^ (A *) = (A *) ^^ (A |^ (m,n))
A1: (A *) ^^ (A |^ (m,n)) c= (A |^ (m,n)) ^^ (A *)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A *) ^^ (A |^ (m,n)) or x in (A |^ (m,n)) ^^ (A *) )
assume  x in (A *) ^^ (A |^ (m,n)) ; ::_thesis: x in (A |^ (m,n)) ^^ (A *)
then consider a, b being Element of E ^omega  such that
A2: a in A * and
A3: b in A |^ (m,n) and
A4: x = a ^ b by FLANG_1:def_1;
consider k being Nat such that
A5: a in A |^ k by A2, FLANG_1:41;
consider mn being Nat such that
A6: ( m <= mn & mn <= n ) and
A7: b in A |^ mn by A3, Th19;
 ( A |^ k c= A * & A |^ mn c= A |^ (m,n) ) by A6, Th20, FLANG_1:42;
then A8: (A |^ mn) ^^ (A |^ k) c= (A |^ (m,n)) ^^ (A *) by FLANG_1:17;
 a ^ b in A |^ (mn + k) by A7, A5, FLANG_1:40;
then  a ^ b in (A |^ mn) ^^ (A |^ k) by FLANG_1:33;
hence  x in (A |^ (m,n)) ^^ (A *) by A4, A8; ::_thesis: verum
end;
 (A |^ (m,n)) ^^ (A *) c= (A *) ^^ (A |^ (m,n))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A |^ (m,n)) ^^ (A *) or x in (A *) ^^ (A |^ (m,n)) )
assume  x in (A |^ (m,n)) ^^ (A *) ; ::_thesis: x in (A *) ^^ (A |^ (m,n))
then consider a, b being Element of E ^omega  such that
A9: a in A |^ (m,n) and
A10: b in A * and
A11: x = a ^ b by FLANG_1:def_1;
consider k being Nat such that
A12: b in A |^ k by A10, FLANG_1:41;
consider mn being Nat such that
A13: ( m <= mn & mn <= n ) and
A14: a in A |^ mn by A9, Th19;
 ( A |^ k c= A * & A |^ mn c= A |^ (m,n) ) by A13, Th20, FLANG_1:42;
then A15: (A |^ k) ^^ (A |^ mn) c= (A *) ^^ (A |^ (m,n)) by FLANG_1:17;
 a ^ b in A |^ (k + mn) by A14, A12, FLANG_1:40;
then  a ^ b in (A |^ k) ^^ (A |^ mn) by FLANG_1:33;
hence  x in (A *) ^^ (A |^ (m,n)) by A11, A15; ::_thesis: verum
end;
hence  (A |^ (m,n)) ^^ (A *) = (A *) ^^ (A |^ (m,n)) by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: FLANG_2:67
for E being set
for A being Subset of (E ^omega)
for m, n being Nat st <%> E in A & m <= n holds
A * = (A *) ^^ (A |^ (m,n))
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for m, n being Nat st <%> E in A & m <= n holds
A * = (A *) ^^ (A |^ (m,n))
let A be Subset of (E ^omega); ::_thesis: for m, n being Nat st <%> E in A & m <= n holds
A * = (A *) ^^ (A |^ (m,n))
let m, n be Nat; ::_thesis: ( <%> E in A & m <= n implies A * = (A *) ^^ (A |^ (m,n)) )
assume that
A1: <%> E in A and
A2: m <= n ; ::_thesis: A * = (A *) ^^ (A |^ (m,n))
A3: ex k being Nat st m + k = n by A2, NAT_1:10;
defpred S1[ Nat] means A * = (A *) ^^ (A |^ (m,(m + $1)));
A4: now__::_thesis:_for_i_being_Nat_st_S1[i]_holds_
S1[i_+_1]
let i be Nat; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A5: S1[i] ; ::_thesis: S1[i + 1]
 A |^ (m,(m + (i + 1))) = (A |^ (m,(m + i))) \/ (A |^ ((m + i) + 1)) by Th26, NAT_1:11;
then (A *) ^^ (A |^ (m,(m + (i + 1)))) = (A *) \/ ((A *) ^^ (A |^ ((m + i) + 1))) by A5, FLANG_1:20
.= (A *) \/ (A *) by A1, FLANG_1:55 ;
hence  S1[i + 1] ; ::_thesis: verum
end;
A * = (A *) ^^ (A |^ m) by A1, FLANG_1:55
.= (A *) ^^ (A |^ (m,(m + 0))) by Th22 ;
then A6: S1[ 0 ] ;
 for i being Nat holds S1[i] from NAT_1:sch_2(A6, A4);
hence  A * = (A *) ^^ (A |^ (m,n)) by A3; ::_thesis: verum
end;

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 *
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for k, m, n being Nat holds (A |^ k) |^ (m,n) c= A *
let A be Subset of (E ^omega); ::_thesis: for k, m, n being Nat holds (A |^ k) |^ (m,n) c= A *
let k, m, n be Nat; ::_thesis: (A |^ k) |^ (m,n) c= A *
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A |^ k) |^ (m,n) or x in A * )
assume  x in (A |^ k) |^ (m,n) ; ::_thesis: x in A *
then consider mn being Nat such that
 m <= mn and
 mn <= n and
A1: x in (A |^ k) |^ mn by Th19;
A2: A |^ (k * mn) c= A * by FLANG_1:42;
 x in A |^ (k * mn) by A1, FLANG_1:34;
hence  x in A * by A2; ::_thesis: verum
end;

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 *
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for m, n, k, l being Nat holds (A |^ (m,n)) |^ (k,l) c= A *
let A be Subset of (E ^omega); ::_thesis: for m, n, k, l being Nat holds (A |^ (m,n)) |^ (k,l) c= A *
let m, n, k, l be Nat; ::_thesis: (A |^ (m,n)) |^ (k,l) c= A *
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A |^ (m,n)) |^ (k,l) or x in A * )
assume  x in (A |^ (m,n)) |^ (k,l) ; ::_thesis: x in A *
then consider kl being Nat such that
 k <= kl and
 kl <= l and
A1: x in (A |^ (m,n)) |^ kl by Th19;
 (A |^ (m,n)) |^ kl c= A * by Th32, FLANG_1:59;
hence  x in A * by A1; ::_thesis: verum
end;

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 & k <= n & l <= n holds
A |^ (k,n) = A |^ (l,n)
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for k, n, l being Nat st <%> E in A & k <= n & l <= n holds
A |^ (k,n) = A |^ (l,n)
let A be Subset of (E ^omega); ::_thesis: for k, n, l being Nat st <%> E in A & k <= n & l <= n holds
A |^ (k,n) = A |^ (l,n)
let k, n, l be Nat; ::_thesis: ( <%> E in A & k <= n & l <= n implies A |^ (k,n) = A |^ (l,n) )
assume that
A1: <%> E in A and
A2: k <= n and
A3: l <= n ; ::_thesis: A |^ (k,n) = A |^ (l,n)
thus A |^ (k,n) = A |^ n by A1, A2, Th34
.= A |^ (l,n) by A1, A3, Th34 ; ::_thesis: verum
end;

begin

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 & B = A |^ k )  }  ;
coherence
 union  {  B where B is Subset of (E ^omega) : ex k being Nat st
( k <= 1 & B = A |^ k )  }  is Subset of (E ^omega)
proof
defpred S1[ set ] means  ex k being Nat st
( k <= 1 & $1 = A |^ k );
reconsider M =  {  B where B is Subset of (E ^omega) : S1[B]  }  as Subset-Family of (E ^omega) from DOMAIN_1:sch_7();
 union M is Subset of (E ^omega) ;
hence  union  {  B where B is Subset of (E ^omega) : ex k being Nat st
( k <= 1 & B = A |^ k )  }  is Subset of (E ^omega) ; ::_thesis: verum
end;
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 & B = A |^ k )  }  ;

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 & x in A |^ k ) )
proof
let E, x be set ; ::_thesis: for A being Subset of (E ^omega) holds
( x in A ? iff ex k being Nat st
( k <= 1 & x in A |^ k ) )
let A be Subset of (E ^omega); ::_thesis: ( x in A ? iff ex k being Nat st
( k <= 1 & x in A |^ k ) )
thus  ( x in A ? implies ex k being Nat st
( k <= 1 & x in A |^ k ) ) ::_thesis: ( ex k being Nat st
( k <= 1 & x in A |^ k ) implies x in A ? )
proof
defpred S1[ set ] means  ex k being Nat st
( k <= 1 & $1 = A |^ k );
assume  x in A ? ; ::_thesis: ex k being Nat st
( k <= 1 & x in A |^ k )
then consider X being set  such that
A1: x in X and
A2: X in  {  B where B is Subset of (E ^omega) : ex k being Nat st
( k <= 1 & B = A |^ k )  }  by TARSKI:def_4;
A3: X in  {  B where B is Subset of (E ^omega) : S1[B]  }  by A2;
 S1[X] from CARD_FIL:sch_1(A3);
hence  ex k being Nat st
( k <= 1 & x in A |^ k ) by A1; ::_thesis: verum
end;
given k being Nat such that A4: ( k <= 1 & x in A |^ k ) ; ::_thesis: x in A ?
defpred S1[ set ] means  ex k being Nat st
( k <= 1 & $1 = A |^ k );
consider B being Subset of (E ^omega) such that
A5: x in B and
A6: S1[B] by A4;
reconsider A =  {  C where C is Subset of (E ^omega) : S1[C]  }  as Subset-Family of (E ^omega) from DOMAIN_1:sch_7();
 B in A by A6;
hence  x in A ? by A5, TARSKI:def_4; ::_thesis: verum
end;

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 ?
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for n being Nat st n <= 1 holds
A |^ n c= A ?
let A be Subset of (E ^omega); ::_thesis: for n being Nat st n <= 1 holds
A |^ n c= A ?
let n be Nat; ::_thesis: ( n <= 1 implies A |^ n c= A ? )
assume  n <= 1 ; ::_thesis: A |^ n c= A ?
then  for x being set st x in A |^ n holds
x in A ? by Th73;
hence  A |^ n c= A ? by TARSKI:def_3; ::_thesis: verum
end;

theorem Th75: :: FLANG_2:75
for E being set
for A being Subset of (E ^omega) holds A ? = (A |^ 0) \/ (A |^ 1)
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds A ? = (A |^ 0) \/ (A |^ 1)
let A be Subset of (E ^omega); ::_thesis: A ? = (A |^ 0) \/ (A |^ 1)
now__::_thesis:_for_x_being_set_holds_
(_x_in_A_?_iff_(_x_in_A_|^_0_or_x_in_A_|^_1_)_)
let x be set ; ::_thesis: ( x in A ? iff ( x in A |^ 0 or x in A |^ 1 ) )
 ( x in A ? iff ex k being Nat st
( ( k = 0 or k = 1 ) & x in A |^ k ) )
proof
thus  ( x in A ? implies ex k being Nat st
( ( k = 0 or k = 1 ) & x in A |^ k ) ) ::_thesis: ( ex k being Nat st
( ( k = 0 or k = 1 ) & x in A |^ k ) implies x in A ? )
proof
assume  x in A ? ; ::_thesis: ex k being Nat st
( ( k = 0 or k = 1 ) & x in A |^ k )
then consider k being Nat such that
A1: k <= 1 and
A2: x in A |^ k by Th73;
 ( k = 0 or k = 1 ) by A1, NAT_1:25;
hence  ex k being Nat st
( ( k = 0 or k = 1 ) & x in A |^ k ) by A2; ::_thesis: verum
end;
given k being Nat such that A3: ( ( k = 0 or k = 1 ) & x in A |^ k ) ; ::_thesis: x in A ?
thus  x in A ? by A3, Th73; ::_thesis: verum
end;
hence  ( x in A ? iff ( x in A |^ 0 or x in A |^ 1 ) ) ; ::_thesis: verum
end;
hence  A ? = (A |^ 0) \/ (A |^ 1) by XBOOLE_0:def_3; ::_thesis: verum
end;

theorem Th76: :: FLANG_2:76
for E being set
for A being Subset of (E ^omega) holds A ? = {(<%> E)} \/ A
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds A ? = {(<%> E)} \/ A
let A be Subset of (E ^omega); ::_thesis: A ? = {(<%> E)} \/ A
 ( A |^ 0 = {(<%> E)} & A |^ 1 = A ) by FLANG_1:24, FLANG_1:25;
hence  A ? = {(<%> E)} \/ A by Th75; ::_thesis: verum
end;

theorem :: FLANG_2:77
for E being set
for A being Subset of (E ^omega) holds A c= A ?
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds A c= A ?
let A be Subset of (E ^omega); ::_thesis: A c= A ?
 A ? = {(<%> E)} \/ A by Th76;
hence  A c= A ? by XBOOLE_1:7; ::_thesis: verum
end;

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 ) )
proof
let x, E be set ; ::_thesis: for A being Subset of (E ^omega) holds
( x in A ? iff ( x = <%> E or x in A ) )
let A be Subset of (E ^omega); ::_thesis: ( x in A ? iff ( x = <%> E or x in A ) )
 ( x in A ? iff x in {(<%> E)} \/ A ) by Th76;
then  ( x in A ? iff ( x in {(<%> E)} or x in A ) ) by XBOOLE_0:def_3;
hence  ( x in A ? iff ( x = <%> E or x in A ) ) by TARSKI:def_1; ::_thesis: verum
end;

theorem Th79: :: FLANG_2:79
for E being set
for A being Subset of (E ^omega) holds A ? = A |^ (0,1)
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds A ? = A |^ (0,1)
let A be Subset of (E ^omega); ::_thesis: A ? = A |^ (0,1)
thus A ? = (A |^ 0) \/ (A |^ (0 + 1)) by Th75
.= A |^ (0,1) by Th28 ; ::_thesis: verum
end;

theorem Th80: :: FLANG_2:80
for E being set
for A being Subset of (E ^omega) holds
( A ? = A iff <%> E in A )
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds
( A ? = A iff <%> E in A )
let A be Subset of (E ^omega); ::_thesis: ( A ? = A iff <%> E in A )
thus  ( A ? = A implies <%> E in A ) ::_thesis: ( <%> E in A implies A ? = A )
proof
assume  A ? = A ; ::_thesis: <%> E in A
then  A = {(<%> E)} \/ A by Th76;
hence  <%> E in A by ZFMISC_1:39; ::_thesis: verum
end;
assume  <%> E in A ; ::_thesis: A ? = A
then  A = {(<%> E)} \/ A by ZFMISC_1:40;
hence  A ? = A by Th76; ::_thesis: verum
end;

registration
let E be set ;
let A be Subset of (E ^omega);
clusterA ?  ->  non empty ;
coherence
 not A ? is empty
proof
 <%> E in A ? by Th78;
hence  not A ? is empty ; ::_thesis: verum
end;
end;

theorem :: FLANG_2:81
for E being set
for A being Subset of (E ^omega) holds (A ?) ? = A ?
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds (A ?) ? = A ?
let A be Subset of (E ^omega); ::_thesis: (A ?) ? = A ?
 <%> E in A ? by Th78;
hence  (A ?) ? = A ? by Th80; ::_thesis: verum
end;

theorem :: FLANG_2:82
for E being set
for A, B being Subset of (E ^omega) st A c= B holds
A ? c= B ?
proof
let E be set ; ::_thesis: for A, B being Subset of (E ^omega) st A c= B holds
A ? c= B ?
let A, B be Subset of (E ^omega); ::_thesis: ( A c= B implies A ? c= B ? )
assume  A c= B ; ::_thesis: A ? c= B ?
then  A |^ (0,1) c= B |^ (0,1) by Th29;
then  A ? c= B |^ (0,1) by Th79;
hence  A ? c= B ? by Th79; ::_thesis: verum
end;

theorem :: FLANG_2:83
for x, E being set
for A being Subset of (E ^omega) st x in A & x <> <%> E holds
A ? <> {(<%> E)}
proof
let x, E be set ; ::_thesis: for A being Subset of (E ^omega) st x in A & x <> <%> E holds
A ? <> {(<%> E)}
let A be Subset of (E ^omega); ::_thesis: ( x in A & x <> <%> E implies A ? <> {(<%> E)} )
assume A1: ( x in A & x <> <%> E ) ; ::_thesis: A ? <> {(<%> E)}
 A ? = A |^ (0,1) by Th79;
hence  A ? <> {(<%> E)} by A1, Th30; ::_thesis: verum
end;

theorem :: FLANG_2:84
for E being set
for A being Subset of (E ^omega) holds
( A ? = {(<%> E)} iff ( A = {} or A = {(<%> E)} ) )
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds
( A ? = {(<%> E)} iff ( A = {} or A = {(<%> E)} ) )
let A be Subset of (E ^omega); ::_thesis: ( A ? = {(<%> E)} iff ( A = {} or A = {(<%> E)} ) )
 A ? = A |^ (0,1) by Th79;
hence  ( A ? = {(<%> E)} iff ( A = {} or A = {(<%> E)} ) ) by Th31; ::_thesis: verum
end;

theorem :: FLANG_2:85
for E being set
for A being Subset of (E ^omega) holds
( (A *) ? = A * & (A ?) * = A * )
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds
( (A *) ? = A * & (A ?) * = A * )
let A be Subset of (E ^omega); ::_thesis: ( (A *) ? = A * & (A ?) * = A * )
thus (A *) ? = {(<%> E)} \/ (A *) by Th76
.= A * by FLANG_1:48, ZFMISC_1:40 ; ::_thesis: (A ?) * = A *
thus (A ?) * = ({(<%> E)} \/ A) * by Th76
.= A * by FLANG_1:48, FLANG_1:68 ; ::_thesis: verum
end;

theorem :: FLANG_2:86
for E being set
for A being Subset of (E ^omega) holds A ? c= A *
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds A ? c= A *
let A be Subset of (E ^omega); ::_thesis: A ? c= A *
 A ? = A |^ (0,1) by Th79;
hence  A ? c= A * by Th32; ::_thesis: verum
end;

theorem :: FLANG_2:87
for E being set
for A, B being Subset of (E ^omega) holds (A /\ B) ? = (A ?) /\ (B ?)
proof
let E be set ; ::_thesis: for A, B being Subset of (E ^omega) holds (A /\ B) ? = (A ?) /\ (B ?)
let A, B be Subset of (E ^omega); ::_thesis: (A /\ B) ? = (A ?) /\ (B ?)
thus (A /\ B) ? = {(<%> E)} \/ (A /\ B) by Th76
.= ({(<%> E)} \/ A) /\ ({(<%> E)} \/ B) by XBOOLE_1:24
.= (A ?) /\ ({(<%> E)} \/ B) by Th76
.= (A ?) /\ (B ?) by Th76 ; ::_thesis: verum
end;

theorem :: FLANG_2:88
for E being set
for A, B being Subset of (E ^omega) holds (A ?) \/ (B ?) = (A \/ B) ?
proof
let E be set ; ::_thesis: for A, B being Subset of (E ^omega) holds (A ?) \/ (B ?) = (A \/ B) ?
let A, B be Subset of (E ^omega); ::_thesis: (A ?) \/ (B ?) = (A \/ B) ?
thus (A \/ B) ? = {(<%> E)} \/ (A \/ B) by Th76
.= (A \/ {(<%> E)}) \/ (B \/ {(<%> E)}) by XBOOLE_1:5
.= (A ?) \/ (B \/ {(<%> E)}) by Th76
.= (A ?) \/ (B ?) by Th76 ; ::_thesis: verum
end;

theorem :: FLANG_2:89
for x, E being set
for A being Subset of (E ^omega) st A ? = {x} holds
x = <%> E
proof
let x, E be set ; ::_thesis: for A being Subset of (E ^omega) st A ? = {x} holds
x = <%> E
let A be Subset of (E ^omega); ::_thesis: ( A ? = {x} implies x = <%> E )
 A ? = A |^ (0,1) by Th79;
hence  ( A ? = {x} implies x = <%> E ) by Th52; ::_thesis: verum
end;

theorem :: FLANG_2:90
for E, x being set
for A being Subset of (E ^omega) holds
( <%x%> in A ? iff <%x%> in A )
proof
let E, x be set ; ::_thesis: for A being Subset of (E ^omega) holds
( <%x%> in A ? iff <%x%> in A )
let A be Subset of (E ^omega); ::_thesis: ( <%x%> in A ? iff <%x%> in A )
 A ? = A |^ (0,1) by Th79;
hence  ( <%x%> in A ? iff <%x%> in A ) by Th53; ::_thesis: verum
end;

theorem :: FLANG_2:91
for E being set
for A being Subset of (E ^omega) holds (A ?) ^^ A = A ^^ (A ?)
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds (A ?) ^^ A = A ^^ (A ?)
let A be Subset of (E ^omega); ::_thesis: (A ?) ^^ A = A ^^ (A ?)
 A ? = A |^ (0,1) by Th79;
hence  (A ?) ^^ A = A ^^ (A ?) by Th36; ::_thesis: verum
end;

theorem :: FLANG_2:92
for E being set
for A being Subset of (E ^omega) holds (A ?) ^^ A = A |^ (1,2)
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds (A ?) ^^ A = A |^ (1,2)
let A be Subset of (E ^omega); ::_thesis: (A ?) ^^ A = A |^ (1,2)
 A ? = A |^ (0,1) by Th79;
then  (A ?) ^^ A = A |^ ((0 + 1),(1 + 1)) by Th38;
hence  (A ?) ^^ A = A |^ (1,2) ; ::_thesis: verum
end;

theorem Th93: :: FLANG_2:93
for E being set
for A being Subset of (E ^omega) holds (A ?) ^^ (A ?) = A |^ (0,2)
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds (A ?) ^^ (A ?) = A |^ (0,2)
let A be Subset of (E ^omega); ::_thesis: (A ?) ^^ (A ?) = A |^ (0,2)
 A ? = A |^ (0,1) by Th79;
then  (A ?) ^^ (A ?) = A |^ ((0 + 0),(1 + 1)) by Th37;
hence  (A ?) ^^ (A ?) = A |^ (0,2) ; ::_thesis: verum
end;

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)
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for k being Nat holds (A ?) |^ k = (A ?) |^ (0,k)
let A be Subset of (E ^omega); ::_thesis: for k being Nat holds (A ?) |^ k = (A ?) |^ (0,k)
let k be Nat; ::_thesis: (A ?) |^ k = (A ?) |^ (0,k)
 <%> E in A ? by Th78;
hence  (A ?) |^ k = (A ?) |^ (0,k) by Th34; ::_thesis: verum
end;

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)
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for k being Nat holds (A ?) |^ k = A |^ (0,k)
let A be Subset of (E ^omega); ::_thesis: for k being Nat holds (A ?) |^ k = A |^ (0,k)
let k be Nat; ::_thesis: (A ?) |^ k = A |^ (0,k)
defpred S1[ Nat] means (A ?) |^ $1 = A |^ (0,$1);
A1: now__::_thesis:_for_k_being_Nat_st_S1[k]_holds_
S1[k_+_1]
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A2: S1[k] ; ::_thesis: S1[k + 1]
(A ?) |^ (k + 1) = ((A ?) |^ k) ^^ ((A ?) |^ 1) by FLANG_1:33
.= (A |^ (0,k)) ^^ (A ?) by A2, FLANG_1:25
.= (A |^ (0,k)) ^^ (A |^ (0,1)) by Th79
.= A |^ ((0 + 0),(k + 1)) by Th37 ;
hence  S1[k + 1] ; ::_thesis: verum
end;
(A ?) |^ 0 = {(<%> E)} by FLANG_1:24
.= A |^ (0,0) by Th45 ;
then A3: S1[ 0 ] ;
 for k being Nat holds S1[k] from NAT_1:sch_2(A3, A1);
hence  (A ?) |^ k = A |^ (0,k) ; ::_thesis: verum
end;

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)
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for m, n being Nat st m <= n holds
(A ?) |^ (m,n) = (A ?) |^ (0,n)
let A be Subset of (E ^omega); ::_thesis: for m, n being Nat st m <= n holds
(A ?) |^ (m,n) = (A ?) |^ (0,n)
let m, n be Nat; ::_thesis: ( m <= n implies (A ?) |^ (m,n) = (A ?) |^ (0,n) )
assume A1: m <= n ; ::_thesis: (A ?) |^ (m,n) = (A ?) |^ (0,n)
 <%> E in A ? by Th78;
hence  (A ?) |^ (m,n) = (A ?) |^ (0,n) by A1, Th72; ::_thesis: verum
end;

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)
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for n being Nat holds (A ?) |^ (0,n) = A |^ (0,n)
let A be Subset of (E ^omega); ::_thesis: for n being Nat holds (A ?) |^ (0,n) = A |^ (0,n)
let n be Nat; ::_thesis: (A ?) |^ (0,n) = A |^ (0,n)
thus (A ?) |^ (0,n) = (A ?) |^ n by Th94
.= A |^ (0,n) by Th95 ; ::_thesis: verum
end;

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)
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for m, n being Nat st m <= n holds
(A ?) |^ (m,n) = A |^ (0,n)
let A be Subset of (E ^omega); ::_thesis: for m, n being Nat st m <= n holds
(A ?) |^ (m,n) = A |^ (0,n)
let m, n be Nat; ::_thesis: ( m <= n implies (A ?) |^ (m,n) = A |^ (0,n) )
assume  m <= n ; ::_thesis: (A ?) |^ (m,n) = A |^ (0,n)
hence (A ?) |^ (m,n) = (A ?) |^ (0,n) by Th96
.= A |^ (0,n) by Th97 ;
::_thesis: verum
end;

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)
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for n being Nat holds (A |^ (1,n)) ? = A |^ (0,n)
let A be Subset of (E ^omega); ::_thesis: for n being Nat holds (A |^ (1,n)) ? = A |^ (0,n)
let n be Nat; ::_thesis: (A |^ (1,n)) ? = A |^ (0,n)
thus (A |^ (1,n)) ? = {(<%> E)} \/ (A |^ (1,n)) by Th76
.= (A |^ (0,0)) \/ (A |^ ((0 + 1),n)) by Th45
.= A |^ (0,n) by Th25 ; ::_thesis: verum
end;

theorem :: FLANG_2:100
for E being set
for A, B being Subset of (E ^omega) st <%> E in A & <%> E in B holds
( A ? c= A ^^ B & A ? c= B ^^ A )
proof
let E be set ; ::_thesis: for A, B being Subset of (E ^omega) st <%> E in A & <%> E in B holds
( A ? c= A ^^ B & A ? c= B ^^ A )
let A, B be Subset of (E ^omega); ::_thesis: ( <%> E in A & <%> E in B implies ( A ? c= A ^^ B & A ? c= B ^^ A ) )
assume that
A1: <%> E in A and
A2: <%> E in B ; ::_thesis: ( A ? c= A ^^ B & A ? c= B ^^ A )
 <%> E in B ^^ A by A1, A2, FLANG_1:15;
then A3: {(<%> E)} c= B ^^ A by ZFMISC_1:31;
 <%> E in A ^^ B by A1, A2, FLANG_1:15;
then A4: {(<%> E)} c= A ^^ B by ZFMISC_1:31;
 A c= B ^^ A by A2, FLANG_1:16;
then A5: {(<%> E)} \/ A c= B ^^ A by A3, XBOOLE_1:8;
 A c= A ^^ B by A2, FLANG_1:16;
then  {(<%> E)} \/ A c= A ^^ B by A4, XBOOLE_1:8;
hence  ( A ? c= A ^^ B & A ? c= B ^^ A ) by A5, Th76; ::_thesis: verum
end;

theorem :: FLANG_2:101
for E being set
for A, B being Subset of (E ^omega) holds
( A c= A ^^ (B ?) & A c= (B ?) ^^ A )
proof
let E be set ; ::_thesis: for A, B being Subset of (E ^omega) holds
( A c= A ^^ (B ?) & A c= (B ?) ^^ A )
let A, B be Subset of (E ^omega); ::_thesis: ( A c= A ^^ (B ?) & A c= (B ?) ^^ A )
 <%> E in B ? by Th78;
hence  ( A c= A ^^ (B ?) & A c= (B ?) ^^ A ) by FLANG_1:16; ::_thesis: verum
end;

theorem :: FLANG_2:102
for E being set
for A, C, B being Subset of (E ^omega) st A c= C ? & B c= C ? holds
A ^^ B c= C |^ (0,2)
proof
let E be set ; ::_thesis: for A, C, B being Subset of (E ^omega) st A c= C ? & B c= C ? holds
A ^^ B c= C |^ (0,2)
let A, C, B be Subset of (E ^omega); ::_thesis: ( A c= C ? & B c= C ? implies A ^^ B c= C |^ (0,2) )
assume  ( A c= C ? & B c= C ? ) ; ::_thesis: A ^^ B c= C |^ (0,2)
then  A ^^ B c= (C ?) ^^ (C ?) by FLANG_1:17;
hence  A ^^ B c= C |^ (0,2) by Th93; ::_thesis: verum
end;

theorem :: FLANG_2:103
for E being set
for A being Subset of (E ^omega)
for n being Nat st <%> E in A & n > 0 holds
A ? c= A |^ n
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for n being Nat st <%> E in A & n > 0 holds
A ? c= A |^ n
let A be Subset of (E ^omega); ::_thesis: for n being Nat st <%> E in A & n > 0 holds
A ? c= A |^ n
let n be Nat; ::_thesis: ( <%> E in A & n > 0 implies A ? c= A |^ n )
assume that
A1: <%> E in A and
A2: n > 0 ; ::_thesis: A ? c= A |^ n
 <%> E in A |^ n by A1, FLANG_1:30;
then A3: {(<%> E)} c= A |^ n by ZFMISC_1:31;
 A c= A |^ n by A1, A2, FLANG_1:35;
then  {(<%> E)} \/ A c= A |^ n by A3, XBOOLE_1:8;
hence  A ? c= A |^ n by Th76; ::_thesis: verum
end;

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 ?)
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for k being Nat holds (A ?) ^^ (A |^ k) = (A |^ k) ^^ (A ?)
let A be Subset of (E ^omega); ::_thesis: for k being Nat holds (A ?) ^^ (A |^ k) = (A |^ k) ^^ (A ?)
let k be Nat; ::_thesis: (A ?) ^^ (A |^ k) = (A |^ k) ^^ (A ?)
thus (A ?) ^^ (A |^ k) = ({(<%> E)} \/ A) ^^ (A |^ k) by Th76
.= ({(<%> E)} ^^ (A |^ k)) \/ (A ^^ (A |^ k)) by FLANG_1:20
.= ({(<%> E)} ^^ (A |^ k)) \/ ((A |^ k) ^^ A) by FLANG_1:32
.= (A |^ k) \/ ((A |^ k) ^^ A) by FLANG_1:13
.= ((A |^ k) ^^ {(<%> E)}) \/ ((A |^ k) ^^ A) by FLANG_1:13
.= (A |^ k) ^^ (A \/ {(<%> E)}) by FLANG_1:20
.= (A |^ k) ^^ (A ?) by Th76 ; ::_thesis: verum
end;

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 *
proof
let E be set ; ::_thesis: for A, B being Subset of (E ^omega) st A c= B * holds
A ? c= B *
let A, B be Subset of (E ^omega); ::_thesis: ( A c= B * implies A ? c= B * )
assume  A c= B * ; ::_thesis: A ? c= B *
then  A |^ (0,1) c= B * by Th64;
hence  A ? c= B * by Th79; ::_thesis: verum
end;

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 ?)
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds (A ?) ^^ (A *) = (A *) ^^ (A ?)
let A be Subset of (E ^omega); ::_thesis: (A ?) ^^ (A *) = (A *) ^^ (A ?)
thus (A ?) ^^ (A *) = (A |^ (0,1)) ^^ (A *) by Th79
.= (A *) ^^ (A |^ (0,1)) by Th66
.= (A *) ^^ (A ?) by Th79 ; ::_thesis: verum
end;

theorem :: FLANG_2:108
for E being set
for A being Subset of (E ^omega) holds (A ?) ^^ (A *) = A *
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds (A ?) ^^ (A *) = A *
let A be Subset of (E ^omega); ::_thesis: (A ?) ^^ (A *) = A *
thus (A ?) ^^ (A *) = ({(<%> E)} \/ A) ^^ (A *) by Th76
.= ({(<%> E)} ^^ (A *)) \/ (A ^^ (A *)) by FLANG_1:20
.= (A *) \/ (A ^^ (A *)) by FLANG_1:13
.= A * by FLANG_1:53, XBOOLE_1:12 ; ::_thesis: verum
end;

theorem :: FLANG_2:109
for E being set
for A being Subset of (E ^omega)
for k being Nat holds (A ?) |^ k c= A *
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for k being Nat holds (A ?) |^ k c= A *
let A be Subset of (E ^omega); ::_thesis: for k being Nat holds (A ?) |^ k c= A *
let k be Nat; ::_thesis: (A ?) |^ k c= A *
 (A ?) |^ k = (A |^ (0,1)) |^ k by Th79;
hence  (A ?) |^ k c= A * by Th32, FLANG_1:59; ::_thesis: verum
end;

theorem :: FLANG_2:110
for E being set
for A being Subset of (E ^omega)
for k being Nat holds (A |^ k) ? c= A *
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for k being Nat holds (A |^ k) ? c= A *
let A be Subset of (E ^omega); ::_thesis: for k being Nat holds (A |^ k) ? c= A *
let k be Nat; ::_thesis: (A |^ k) ? c= A *
 (A |^ k) ? = (A |^ k) |^ (0,1) by Th79;
hence  (A |^ k) ? c= A * by Th69; ::_thesis: verum
end;

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 ?)
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for m, n being Nat holds (A ?) ^^ (A |^ (m,n)) = (A |^ (m,n)) ^^ (A ?)
let A be Subset of (E ^omega); ::_thesis: for m, n being Nat holds (A ?) ^^ (A |^ (m,n)) = (A |^ (m,n)) ^^ (A ?)
let m, n be Nat; ::_thesis: (A ?) ^^ (A |^ (m,n)) = (A |^ (m,n)) ^^ (A ?)
 (A |^ (0,1)) ^^ (A |^ (m,n)) = (A |^ (m,n)) ^^ (A |^ (0,1)) by Th39;
then  (A ?) ^^ (A |^ (m,n)) = (A |^ (m,n)) ^^ (A |^ (0,1)) by Th79;
hence  (A ?) ^^ (A |^ (m,n)) = (A |^ (m,n)) ^^ (A ?) by Th79; ::_thesis: verum
end;

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))
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for k being Nat holds (A ?) ^^ (A |^ k) = A |^ (k,(k + 1))
let A be Subset of (E ^omega); ::_thesis: for k being Nat holds (A ?) ^^ (A |^ k) = A |^ (k,(k + 1))
let k be Nat; ::_thesis: (A ?) ^^ (A |^ k) = A |^ (k,(k + 1))
(A |^ (0,1)) ^^ (A |^ k) = (A |^ (0,1)) ^^ (A |^ (k,k)) by Th22
.= A |^ ((0 + k),(1 + k)) by Th37 ;
hence  (A ?) ^^ (A |^ k) = A |^ (k,(k + 1)) by Th79; ::_thesis: verum
end;

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 *
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for m, n being Nat holds (A ?) |^ (m,n) c= A *
let A be Subset of (E ^omega); ::_thesis: for m, n being Nat holds (A ?) |^ (m,n) c= A *
let m, n be Nat; ::_thesis: (A ?) |^ (m,n) c= A *
percases ( m <= n or m > n ) ;
suppose m <= n ; ::_thesis: (A ?) |^ (m,n) c= A *
then  (A ?) |^ (m,n) = A |^ (0,n) by Th98;
hence  (A ?) |^ (m,n) c= A * by Th32; ::_thesis: verum
end;
suppose m > n ; ::_thesis: (A ?) |^ (m,n) c= A *
then  (A ?) |^ (m,n) = {} by Th21;
hence  (A ?) |^ (m,n) c= A * by XBOOLE_1:2; ::_thesis: verum
end;
end;
end;

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 *
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for m, n being Nat holds (A |^ (m,n)) ? c= A *
let A be Subset of (E ^omega); ::_thesis: for m, n being Nat holds (A |^ (m,n)) ? c= A *
let m, n be Nat; ::_thesis: (A |^ (m,n)) ? c= A *
 (A |^ (m,n)) ? = (A |^ (m,n)) |^ (0,1) by Th79;
hence  (A |^ (m,n)) ? c= A * by Th71; ::_thesis: verum
end;

theorem :: FLANG_2:115
for E being set
for A being Subset of (E ^omega) holds A ? = (A \ {(<%> E)}) ?
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds A ? = (A \ {(<%> E)}) ?
let A be Subset of (E ^omega); ::_thesis: A ? = (A \ {(<%> E)}) ?
thus A ? = {(<%> E)} \/ A by Th76
.= {(<%> E)} \/ (A \ {(<%> E)}) by XBOOLE_1:39
.= (A \ {(<%> E)}) ? by Th76 ; ::_thesis: verum
end;

theorem :: FLANG_2:116
for E being set
for A, B being Subset of (E ^omega) st A c= B ? holds
A ? c= B ?
proof
let E be set ; ::_thesis: for A, B being Subset of (E ^omega) st A c= B ? holds
A ? c= B ?
let A, B be Subset of (E ^omega); ::_thesis: ( A c= B ? implies A ? c= B ? )
 <%> E in B ? by Th78;
then A1: {(<%> E)} c= B ? by ZFMISC_1:31;
assume  A c= B ? ; ::_thesis: A ? c= B ?
then  {(<%> E)} \/ A c= B ? by A1, XBOOLE_1:8;
hence  A ? c= B ? by Th76; ::_thesis: verum
end;

theorem :: FLANG_2:117
for E being set
for A, B being Subset of (E ^omega) st A c= B ? holds
B ? = (B \/ A) ?
proof
let E be set ; ::_thesis: for A, B being Subset of (E ^omega) st A c= B ? holds
B ? = (B \/ A) ?
let A, B be Subset of (E ^omega); ::_thesis: ( A c= B ? implies B ? = (B \/ A) ? )
assume A1: A c= B ? ; ::_thesis: B ? = (B \/ A) ?
thus (B \/ A) ? = {(<%> E)} \/ (B \/ A) by Th76
.= ({(<%> E)} \/ B) \/ A by XBOOLE_1:4
.= (B ?) \/ A by Th76
.= B ? by A1, XBOOLE_1:12 ; ::_thesis: verum
end;