:: by Micha{\l} Trybulec

::

:: Received October 9, 2007

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

theorem :: FLANG_3:1

for E being set

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

( (A *) ^^ B c= A * & B ^^ (A *) c= A * )

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

( (A *) ^^ B c= A * & B ^^ (A *) c= A * )

proof end;

definition

let E be set ;

let A be Subset of (E ^omega);

let n be Nat;

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

( n <= m & B = A |^ m ) } is Subset of (E ^omega)

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

let n be Nat;

func A |^.. n -> Subset of (E ^omega) equals :: FLANG_3:def 1

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

( n <= m & B = A |^ m ) } ;

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

( n <= m & B = A |^ m ) } ;

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

( n <= m & B = A |^ m ) } is Subset of (E ^omega)

proof end;

:: deftheorem defines |^.. FLANG_3:def 1 :

for E being set

for A being Subset of (E ^omega)

for n being Nat holds A |^.. n = union { B where B is Subset of (E ^omega) : ex m being Nat st

( n <= m & B = A |^ m ) } ;

for E being set

for A being Subset of (E ^omega)

for n being Nat holds A |^.. n = union { B where B is Subset of (E ^omega) : ex m being Nat st

( n <= m & B = A |^ m ) } ;

:: At least n Occurences

:: Properties of |^.. n

:: Properties of |^.. n

theorem Th2: :: FLANG_3:2

for E, x being set

for A being Subset of (E ^omega)

for n being Nat holds

( x in A |^.. n iff ex m being Nat st

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

for A being Subset of (E ^omega)

for n being Nat holds

( x in A |^.. n iff ex m being Nat st

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

proof end;

theorem Th4: :: FLANG_3:4

for E being set

for A being Subset of (E ^omega)

for n being Nat holds

( A |^.. n = {} iff ( n > 0 & A = {} ) )

for A being Subset of (E ^omega)

for n being Nat holds

( A |^.. n = {} iff ( n > 0 & A = {} ) )

proof end;

theorem Th5: :: FLANG_3:5

for E being set

for A being Subset of (E ^omega)

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

A |^.. n c= A |^.. m

for A being Subset of (E ^omega)

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

A |^.. n c= A |^.. m

proof end;

theorem Th6: :: FLANG_3:6

for E being set

for A being Subset of (E ^omega)

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

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

for A being Subset of (E ^omega)

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

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

proof end;

theorem Th7: :: FLANG_3:7

for E being set

for A being Subset of (E ^omega)

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

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

for A being Subset of (E ^omega)

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

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

proof end;

theorem :: FLANG_3:8

for E being set

for A being Subset of (E ^omega)

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

for A being Subset of (E ^omega)

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

proof end;

theorem Th10: :: FLANG_3:10

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 Th11: :: FLANG_3:11

for E being set

for A being Subset of (E ^omega)

for n being Nat holds

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

for A being Subset of (E ^omega)

for n being Nat holds

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

proof end;

theorem :: FLANG_3:12

for E being set

for A being Subset of (E ^omega)

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

for A being Subset of (E ^omega)

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

proof end;

theorem Th13: :: FLANG_3:13

for E being set

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

for n being Nat st A c= B holds

A |^.. n c= B |^.. n

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

for n being Nat st A c= B holds

A |^.. n c= B |^.. n

proof end;

theorem Th14: :: FLANG_3:14

for E, x being set

for A being Subset of (E ^omega)

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

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

for A being Subset of (E ^omega)

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

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

proof end;

theorem Th15: :: FLANG_3:15

for E being set

for A being Subset of (E ^omega)

for n being Nat holds

( A |^.. n = {(<%> E)} iff ( A = {(<%> E)} or ( n = 0 & A = {} ) ) )

for A being Subset of (E ^omega)

for n being Nat holds

( A |^.. n = {(<%> E)} iff ( A = {(<%> E)} or ( n = 0 & A = {} ) ) )

proof end;

theorem Th16: :: FLANG_3:16

for E being set

for A being Subset of (E ^omega)

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

for A being Subset of (E ^omega)

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

proof end;

theorem Th17: :: FLANG_3:17

for E being set

for A being Subset of (E ^omega)

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

for A being Subset of (E ^omega)

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

proof end;

theorem Th18: :: FLANG_3:18

for E being set

for A being Subset of (E ^omega)

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

for A being Subset of (E ^omega)

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

proof end;

theorem Th19: :: FLANG_3:19

for E being set

for A being Subset of (E ^omega)

for m, n being Nat st n > 0 holds

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

for A being Subset of (E ^omega)

for m, n being Nat st n > 0 holds

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

proof end;

theorem Th21: :: FLANG_3:21

for E being set

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

for m, n being Nat st A c= C |^.. m & B c= C |^.. n holds

A ^^ B c= C |^.. (m + n)

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

for m, n being Nat st A c= C |^.. m & B c= C |^.. n holds

A ^^ B c= C |^.. (m + n)

proof end;

theorem Th22: :: FLANG_3:22

for E being set

for A being Subset of (E ^omega)

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

for A being Subset of (E ^omega)

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

proof end;

theorem Th23: :: FLANG_3:23

for E being set

for A being Subset of (E ^omega)

for n being Nat holds A ^^ (A |^.. n) = (A |^.. n) ^^ A

for A being Subset of (E ^omega)

for n being Nat holds A ^^ (A |^.. n) = (A |^.. n) ^^ A

proof end;

theorem Th24: :: FLANG_3:24

for E being set

for A being Subset of (E ^omega)

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

for A being Subset of (E ^omega)

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

proof end;

theorem Th25: :: FLANG_3:25

for E being set

for A being Subset of (E ^omega)

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

for A being Subset of (E ^omega)

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

proof end;

theorem :: FLANG_3:26

for E being set

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

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

( A c= A ^^ (B |^.. n) & A c= (B |^.. n) ^^ A )

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

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

( A c= A ^^ (B |^.. n) & A c= (B |^.. n) ^^ A )

proof end;

theorem Th27: :: FLANG_3:27

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 Th28: :: FLANG_3:28

for E being set

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

for k, n being Nat st A c= B |^.. k & n > 0 holds

A |^ n c= B |^.. k

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

for k, n being Nat st A c= B |^.. k & n > 0 holds

A |^ n c= B |^.. k

proof end;

theorem Th29: :: FLANG_3:29

for E being set

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

for k, n being Nat st A c= B |^.. k & n > 0 holds

A |^.. n c= B |^.. k

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

for k, n being Nat st A c= B |^.. k & n > 0 holds

A |^.. n c= B |^.. k

proof end;

theorem Th32: :: FLANG_3:32

for E being set

for A being Subset of (E ^omega)

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

for A being Subset of (E ^omega)

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

proof end;

theorem Th33: :: FLANG_3:33

for E being set

for A being Subset of (E ^omega)

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

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

for A being Subset of (E ^omega)

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

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

proof end;

theorem :: FLANG_3:34

for E being set

for A being Subset of (E ^omega)

for k, l being Nat st k <= l holds

(A *) ^^ (A |^ (k,l)) = A |^.. k

for A being Subset of (E ^omega)

for k, l being Nat st k <= l holds

(A *) ^^ (A |^ (k,l)) = A |^.. k

proof end;

theorem Th35: :: FLANG_3:35

for E being set

for A being Subset of (E ^omega)

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

for A being Subset of (E ^omega)

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

proof end;

theorem :: FLANG_3:36

for E being set

for A being Subset of (E ^omega)

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

for A being Subset of (E ^omega)

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

proof end;

theorem Th37: :: FLANG_3:37

for E being set

for C being Subset of (E ^omega)

for a, b being Element of E ^omega

for m, n being Nat st a in C |^.. m & b in C |^.. n holds

a ^ b in C |^.. (m + n)

for C being Subset of (E ^omega)

for a, b being Element of E ^omega

for m, n being Nat st a in C |^.. m & b in C |^.. n holds

a ^ b in C |^.. (m + n)

proof end;

theorem Th38: :: FLANG_3:38

for E, x being set

for A being Subset of (E ^omega)

for k being Nat st A |^.. k = {x} holds

x = <%> E

for A being Subset of (E ^omega)

for k being Nat st A |^.. k = {x} holds

x = <%> E

proof end;

theorem :: FLANG_3:39

for E being set

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

for n being Nat st A c= B * holds

A |^.. n c= B *

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

for n being Nat st A c= B * holds

A |^.. n c= B *

proof end;

theorem Th40: :: FLANG_3:40

for E being set

for A being Subset of (E ^omega)

for k being Nat holds

( A ? c= A |^.. k iff ( k = 0 or <%> E in A ) )

for A being Subset of (E ^omega)

for k being Nat holds

( A ? c= A |^.. k iff ( k = 0 or <%> E in A ) )

proof end;

theorem Th41: :: FLANG_3:41

for E being set

for A being Subset of (E ^omega)

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

for A being Subset of (E ^omega)

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

proof end;

theorem :: FLANG_3:42

for E being set

for A being Subset of (E ^omega)

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

for A being Subset of (E ^omega)

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

proof end;

theorem :: FLANG_3:43

for E being set

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

for k being Nat st B c= A * holds

( (A |^.. k) ^^ B c= A |^.. k & B ^^ (A |^.. k) c= A |^.. k )

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

for k being Nat st B c= A * holds

( (A |^.. k) ^^ B c= A |^.. k & B ^^ (A |^.. k) c= A |^.. k )

proof end;

theorem Th44: :: FLANG_3:44

for E being set

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

for k being Nat holds (A /\ B) |^.. k c= (A |^.. k) /\ (B |^.. k)

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

for k being Nat holds (A /\ B) |^.. k c= (A |^.. k) /\ (B |^.. k)

proof end;

theorem Th45: :: FLANG_3:45

for E being set

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

for k being Nat holds (A |^.. k) \/ (B |^.. k) c= (A \/ B) |^.. k

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

for k being Nat holds (A |^.. k) \/ (B |^.. k) c= (A \/ B) |^.. k

proof end;

theorem Th46: :: FLANG_3:46

for E, x being set

for A being Subset of (E ^omega)

for k being Nat holds

( <%x%> in A |^.. k iff ( <%x%> in A & ( <%> E in A or k <= 1 ) ) )

for A being Subset of (E ^omega)

for k being Nat holds

( <%x%> in A |^.. k iff ( <%x%> in A & ( <%> E in A or k <= 1 ) ) )

proof end;

theorem Th47: :: FLANG_3:47

for E being set

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

for k being Nat st A c= B |^.. k holds

B |^.. k = (B \/ A) |^.. k

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

for k being Nat st A c= B |^.. k holds

B |^.. k = (B \/ A) |^.. k

proof end;

:: Positive Closure

:: 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 n being Nat st

( n > 0 & B = A |^ n ) } is Subset of (E ^omega)

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

func A + -> Subset of (E ^omega) equals :: FLANG_3:def 2

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

( n > 0 & B = A |^ n ) } ;

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

( n > 0 & B = A |^ n ) } ;

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

( n > 0 & B = A |^ n ) } is Subset of (E ^omega)

proof end;

:: deftheorem defines + FLANG_3: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 n being Nat st

( n > 0 & B = A |^ n ) } ;

for E being set

for A being Subset of (E ^omega) holds A + = union { B where B is Subset of (E ^omega) : ex n being Nat st

( n > 0 & B = A |^ n ) } ;

:: Positive Closure

:: Properties of +

:: Properties of +

theorem Th48: :: FLANG_3:48

for E, x being set

for A being Subset of (E ^omega) holds

( x in A + iff ex n being Nat st

( n > 0 & x in A |^ n ) )

for A being Subset of (E ^omega) holds

( x in A + iff ex n being Nat st

( n > 0 & x in A |^ n ) )

proof end;

theorem :: FLANG_3:54

for E being set

for A being Subset of (E ^omega)

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

for A being Subset of (E ^omega)

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

proof end;

theorem Th66: :: FLANG_3:66

for E being set

for C being Subset of (E ^omega)

for a, b being Element of E ^omega st a in C + & b in C + holds

a ^ b in C +

for C being Subset of (E ^omega)

for a, b being Element of E ^omega st a in C + & b in C + holds

a ^ b in C +

proof end;

theorem :: FLANG_3:71

for E being set

for A being Subset of (E ^omega)

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

for A being Subset of (E ^omega)

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

proof end;

theorem Th72: :: FLANG_3:72

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_3:73

for E being set

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

( A c= A ^^ (B +) & A c= (B +) ^^ A )

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

( A c= A ^^ (B +) & A c= (B +) ^^ A )

proof end;

theorem Th75: :: FLANG_3:75

for E being set

for A being Subset of (E ^omega)

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

for A being Subset of (E ^omega)

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

proof end;

theorem :: FLANG_3:77

for E being set

for A being Subset of (E ^omega)

for k, l being Nat st k <= l holds

(A +) ^^ (A |^ (k,l)) = A |^.. (k + 1)

for A being Subset of (E ^omega)

for k, l being Nat st k <= l holds

(A +) ^^ (A |^ (k,l)) = A |^.. (k + 1)

proof end;

theorem :: FLANG_3:78

for E being set

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

for n being Nat st A c= B + & n > 0 holds

A |^ n c= B +

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

for n being Nat st A c= B + & n > 0 holds

A |^ n c= B +

proof end;

theorem :: FLANG_3:85

for E being set

for A being Subset of (E ^omega)

for m, n being Nat st m > 0 holds

A |^ (m,n) c= A +

for A being Subset of (E ^omega)

for m, n being Nat st m > 0 holds

A |^ (m,n) c= A +

proof end;

theorem :: FLANG_3:88

for E being set

for A being Subset of (E ^omega)

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

for A being Subset of (E ^omega)

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

proof end;

theorem :: FLANG_3:89

for E being set

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

for n being Nat st A c= B + & n > 0 holds

A |^.. n c= B +

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

for n being Nat st A c= B + & n > 0 holds

A |^.. n c= B +

proof end;

theorem Th90: :: FLANG_3:90

for E being set

for A being Subset of (E ^omega)

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

for A being Subset of (E ^omega)

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

proof end;

theorem :: FLANG_3:91

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_3:93

for E being set

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

( (A +) ^^ B c= A + & B ^^ (A +) c= A + )

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

( (A +) ^^ B c= A + & B ^^ (A +) c= A + )

proof end;

:: Definition of |^.. n