:: by Micha{\l} Trybulec

::

:: Received June 6, 2007

:: Copyright (c) 2007-2019 Association of Mizar Users

:: Preliminaries - Numbers:

theorem Th1: :: FLANG_2:1

for i, k, m, n being Nat st m + k <= i & i <= n + k holds

ex mn being Nat st

( mn + k = i & m <= mn & mn <= n )

ex mn being Nat st

( mn + k = i & m <= mn & mn <= n )

proof end;

theorem Th2: :: FLANG_2:2

for i, k, l, m, n 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 )

ex mn, kl being Nat st

( mn + kl = i & m <= mn & mn <= n & k <= kl & kl <= l )

proof end;

:: Preliminaries - Sequences:

:: Addenda - FLANG_1:

theorem :: FLANG_2:5

for E, x being set

for A, B being Subset of (E ^omega) st ( x in A or x in B ) & x <> <%> E holds

A ^^ B <> {(<%> E)}

for A, B being Subset of (E ^omega) st ( x in A or x in B ) & x <> <%> E holds

A ^^ B <> {(<%> E)}

proof end;

theorem :: FLANG_2:6

for E, x 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 ) ) )

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 end;

theorem Th7: :: FLANG_2:7

for E, x 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)}

for A being Subset of (E ^omega)

for n being Nat st x in A & x <> <%> E & n > 0 holds

A |^ n <> {(<%> E)}

proof 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 ) )

for A being Subset of (E ^omega)

for n being Nat holds

( <%> E in A |^ n iff ( n = 0 or <%> E in A ) )

proof end;

theorem Th9: :: FLANG_2:9

for E, x 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 ) ) )

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 end;

theorem Th10: :: FLANG_2:10

for E, x 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

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 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

for A being Subset of (E ^omega)

for m, n being Nat holds (A |^ m) |^ n = (A |^ n) |^ m

proof 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)

for A being Subset of (E ^omega)

for m, n being Nat holds (A |^ m) ^^ (A |^ n) = (A |^ n) ^^ (A |^ m)

proof end;

theorem :: FLANG_2:13

for E being set

for A, B being Subset of (E ^omega)

for l being Nat st <%> E in B holds

( A c= A ^^ (B |^ l) & A c= (B |^ l) ^^ A )

for A, B 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 end;

theorem :: FLANG_2:14

for E being set

for A, B, C 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)

for A, B, C 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 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 *

for A being Subset of (E ^omega)

for n being Nat st <%> E in A & n > 0 holds

(A |^ n) * = A *

proof 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

for A being Subset of (E ^omega)

for n being Nat st <%> E in A holds

(A |^ n) * = (A *) |^ n

proof end;

:: Union of a Range of Powers

:: Definition of |^ (n, m)

:: Definition of |^ (n, m)

definition

let E be set ;

let A be Subset of (E ^omega);

let m, n be Nat;

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)

end;
let A be Subset of (E ^omega);

let m, n be Nat;

func A |^ (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 ) } ;

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 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 ) } ;

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 ) } ;

:: Union of a Range of Powers

:: Properties of |^ (n, m)

:: Properties of |^ (n, m)

theorem Th19: :: FLANG_2:19

for E, x being set

for A being Subset of (E ^omega)

for m, n being Nat holds

( x in A |^ (m,n) iff ex k being Nat st

( m <= k & k <= n & x in A |^ k ) )

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 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 = {} ) ) )

for A being Subset of (E ^omega)

for m, n being Nat holds

( A |^ (m,n) = {} iff ( m > n or ( m > 0 & A = {} ) ) )

proof end;

theorem Th23: :: FLANG_2:23

for E being set

for A being Subset of (E ^omega)

for k, l, m, n being Nat st m <= k & l <= n holds

A |^ (k,l) c= A |^ (m,n)

for A being Subset of (E ^omega)

for k, l, m, n being Nat st m <= k & l <= n holds

A |^ (k,l) c= A |^ (m,n)

proof end;

theorem :: FLANG_2:24

for E being set

for A being Subset of (E ^omega)

for k, m, n being Nat st m <= k & k <= n holds

A |^ (m,n) = (A |^ (m,k)) \/ (A |^ (k,n))

for A being Subset of (E ^omega)

for k, m, n being Nat st m <= k & k <= n holds

A |^ (m,n) = (A |^ (m,k)) \/ (A |^ (k,n))

proof end;

theorem Th25: :: FLANG_2:25

for E being set

for A being Subset of (E ^omega)

for k, m, n being Nat st m <= k & k <= n holds

A |^ (m,n) = (A |^ (m,k)) \/ (A |^ ((k + 1),n))

for A being Subset of (E ^omega)

for k, m, n being Nat st m <= k & k <= n holds

A |^ (m,n) = (A |^ (m,k)) \/ (A |^ ((k + 1),n))

proof 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))

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 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))

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 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))

for A being Subset of (E ^omega)

for n being Nat holds A |^ (n,(n + 1)) = (A |^ n) \/ (A |^ (n + 1))

proof 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)

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 end;

theorem Th30: :: FLANG_2:30

for E, x 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)}

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 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 = {} ) ) )

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 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 ) ) )

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 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

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 end;

theorem Th35: :: FLANG_2:35

for E being set

for A being Subset of (E ^omega)

for k, m, n being Nat holds (A |^ (m,n)) ^^ (A |^ k) = (A |^ k) ^^ (A |^ (m,n))

for A being Subset of (E ^omega)

for k, m, n being Nat holds (A |^ (m,n)) ^^ (A |^ k) = (A |^ k) ^^ (A |^ (m,n))

proof 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))

for A being Subset of (E ^omega)

for m, n being Nat holds (A |^ (m,n)) ^^ A = A ^^ (A |^ (m,n))

proof end;

theorem Th37: :: FLANG_2:37

for E being set

for A being Subset of (E ^omega)

for k, l, m, n being Nat st m <= n & k <= l holds

(A |^ (m,n)) ^^ (A |^ (k,l)) = A |^ ((m + k),(n + l))

for A being Subset of (E ^omega)

for k, l, m, n being Nat st m <= n & k <= l holds

(A |^ (m,n)) ^^ (A |^ (k,l)) = A |^ ((m + k),(n + l))

proof 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

for A being Subset of (E ^omega)

for m, n being Nat holds A |^ ((m + 1),(n + 1)) = (A |^ (m,n)) ^^ A

proof end;

theorem Th39: :: FLANG_2:39

for E being set

for A being Subset of (E ^omega)

for k, l, m, n being Nat holds (A |^ (m,n)) ^^ (A |^ (k,l)) = (A |^ (k,l)) ^^ (A |^ (m,n))

for A being Subset of (E ^omega)

for k, l, m, n being Nat holds (A |^ (m,n)) ^^ (A |^ (k,l)) = (A |^ (k,l)) ^^ (A |^ (m,n))

proof end;

theorem Th40: :: FLANG_2:40

for E being set

for A being Subset of (E ^omega)

for k, m, n being Nat holds (A |^ (m,n)) |^ k = A |^ ((m * k),(n * k))

for A being Subset of (E ^omega)

for k, m, n being Nat holds (A |^ (m,n)) |^ k = A |^ ((m * k),(n * k))

proof 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))

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 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))

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 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

for A being Subset of (E ^omega)

for k, m, n being Nat holds (A |^ k) |^ (m,n) c= (A |^ (m,n)) |^ k

proof 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))

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 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}

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 end;

theorem Th52: :: FLANG_2:52

for E, x being set

for A being Subset of (E ^omega)

for m, n being Nat st m <> n & A |^ (m,n) = {x} holds

x = <%> E

for A being Subset of (E ^omega)

for m, n being Nat st m <> n & A |^ (m,n) = {x} holds

x = <%> E

proof end;

theorem Th53: :: FLANG_2:53

for E, x 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 ) ) ) )

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 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))

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 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)

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 end;

theorem :: FLANG_2:56

for E being set

for A being Subset of (E ^omega)

for k, l, m, n being Nat holds (A |^ (m,n)) |^ (k,l) c= A |^ ((m * k),(n * l))

for A being Subset of (E ^omega)

for k, l, m, n being Nat holds (A |^ (m,n)) |^ (k,l) c= A |^ ((m * k),(n * l))

proof end;

theorem :: FLANG_2:57

for E being set

for A, B 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 )

for A, B 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 end;

theorem :: FLANG_2:58

for E being set

for A, B, C being Subset of (E ^omega)

for k, l, m, n 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))

for A, B, C being Subset of (E ^omega)

for k, l, m, n 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 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 *

for A being Subset of (E ^omega)

for m, n being Nat st m <= n & n > 0 holds

(A *) |^ (m,n) = A *

proof 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 *

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 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)

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 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 *

for A, B being Subset of (E ^omega)

for m, n being Nat st A c= B * holds

A |^ (m,n) c= B *

proof end;

theorem :: FLANG_2:65

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))

for A being Subset of (E ^omega)

for m, n being Nat holds (A |^ (m,n)) ^^ (A *) = (A *) ^^ (A |^ (m,n))

proof 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))

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 end;

theorem :: FLANG_2:68

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 *

for A being Subset of (E ^omega)

for k, m, n being Nat holds (A |^ k) |^ (m,n) c= A *

proof end;

theorem :: FLANG_2:70

theorem Th71: :: FLANG_2:71

for E being set

for A being Subset of (E ^omega)

for k, l, m, n being Nat holds (A |^ (m,n)) |^ (k,l) c= A *

for A being Subset of (E ^omega)

for k, l, m, n being Nat holds (A |^ (m,n)) |^ (k,l) c= A *

proof end;

theorem Th72: :: FLANG_2:72

for E being set

for A being Subset of (E ^omega)

for k, l, n being Nat st <%> E in A & k <= n & l <= n holds

A |^ (k,n) = A |^ (l,n)

for A being Subset of (E ^omega)

for k, l, n being Nat st <%> E in A & k <= n & l <= n holds

A |^ (k,n) = A |^ (l,n)

proof end;

:: Optional Occurrence

:: Definition of ?

:: Definition of ?

definition

let E be set ;

let A be Subset of (E ^omega);

union { B where B is Subset of (E ^omega) : ex k being Nat st

( k <= 1 & B = A |^ k ) } is Subset of (E ^omega)

end;
let A be Subset of (E ^omega);

func A ? -> 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 ) } ;

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 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 ) } ;

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 ) } ;

:: Optional Occurrence

:: Properties of ?

:: Properties of ?

theorem Th73: :: FLANG_2:73

for E, x being set

for A being Subset of (E ^omega) holds

( x in A ? iff ex k being Nat st

( k <= 1 & x in A |^ k ) )

for A being Subset of (E ^omega) holds

( x in A ? iff ex k being Nat st

( k <= 1 & x in A |^ k ) )

proof end;

theorem :: FLANG_2:74

registration
end;

theorem :: FLANG_2:84

for E being set

for A being Subset of (E ^omega) holds

( A ? = {(<%> E)} iff ( A = {} or A = {(<%> E)} ) )

for A being Subset of (E ^omega) holds

( A ? = {(<%> E)} iff ( A = {} or A = {(<%> E)} ) )

proof 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)

for A being Subset of (E ^omega)

for m, n being Nat st m <= n holds

(A ?) |^ (m,n) = (A ?) |^ (0,n)

proof 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)

for A being Subset of (E ^omega)

for m, n being Nat st m <= n holds

(A ?) |^ (m,n) = A |^ (0,n)

proof 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 )

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 end;

theorem :: FLANG_2:102

for E being set

for A, B, C being Subset of (E ^omega) st A c= C ? & B c= C ? holds

A ^^ B c= C |^ (0,2)

for A, B, C being Subset of (E ^omega) st A c= C ? & B c= C ? holds

A ^^ B c= C |^ (0,2)

proof 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

for A being Subset of (E ^omega)

for n being Nat st <%> E in A & n > 0 holds

A ? c= A |^ n

proof 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 ?)

for A being Subset of (E ^omega)

for k being Nat holds (A ?) ^^ (A |^ k) = (A |^ k) ^^ (A ?)

proof end;

theorem :: FLANG_2:106

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 ?)

for A being Subset of (E ^omega)

for m, n being Nat holds (A ?) ^^ (A |^ (m,n)) = (A |^ (m,n)) ^^ (A ?)

proof 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))

for A being Subset of (E ^omega)

for k being Nat holds (A ?) ^^ (A |^ k) = A |^ (k,(k + 1))

proof end;