:: FLANG_3 semantic presentation begin theorem :: FLANG_3:1 for E being set for B, A being Subset of (E ^omega) st B c= A * holds ( (A *) ^^ B c= A * & B ^^ (A *) c= A * ) proof let E be set ; ::_thesis: for B, A being Subset of (E ^omega) st B c= A * holds ( (A *) ^^ B c= A * & B ^^ (A *) c= A * ) let B, A be Subset of (E ^omega); ::_thesis: ( B c= A * implies ( (A *) ^^ B c= A * & B ^^ (A *) c= A * ) ) assume A1: B c= A * ; ::_thesis: ( (A *) ^^ B c= A * & B ^^ (A *) c= A * ) then A2: B ^^ (A *) c= (A *) ^^ (A *) by FLANG_1:17; (A *) ^^ B c= (A *) ^^ (A *) by A1, FLANG_1:17; hence ( (A *) ^^ B c= A * & B ^^ (A *) c= A * ) by A2, FLANG_1:63; ::_thesis: verum end; begin definition let E be set ; let A be Subset of (E ^omega); let n be Nat; funcA |^.. 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 ) } is Subset of (E ^omega) proof defpred S1[ set ] means ex m being Nat st ( n <= m & $1 = A |^ m ); 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 m being Nat st ( n <= m & B = A |^ m ) } is Subset of (E ^omega) ; ::_thesis: verum end; 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 ) } ; 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 ) ) proof let E, x be set ; ::_thesis: 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 ) ) let A be Subset of (E ^omega); ::_thesis: for n being Nat holds ( x in A |^.. n iff ex m being Nat st ( n <= m & x in A |^ m ) ) let n be Nat; ::_thesis: ( x in A |^.. n iff ex m being Nat st ( n <= m & x in A |^ m ) ) thus ( x in A |^.. n implies ex m being Nat st ( n <= m & x in A |^ m ) ) ::_thesis: ( ex m being Nat st ( n <= m & x in A |^ m ) implies x in A |^.. n ) proof defpred S1[ set ] means ex m being Nat st ( n <= m & $1 = A |^ m ); assume x in A |^.. n ; ::_thesis: ex m being Nat st ( n <= m & x in A |^ m ) then consider X being set such that A1: x in X and A2: X in { B where B is Subset of (E ^omega) : ex m being Nat st ( n <= m & B = A |^ m ) } 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 m being Nat st ( n <= m & x in A |^ m ) by A1; ::_thesis: verum end; given m being Nat such that A4: n <= m and A5: x in A |^ m ; ::_thesis: x in A |^.. n defpred S1[ set ] means ex m being Nat st ( n <= m & $1 = A |^ m ); consider B being Subset of (E ^omega) such that A6: x in B and A7: S1[B] by A4, A5; 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 A7; hence x in A |^.. n by A6, TARSKI:def_4; ::_thesis: verum end; theorem Th3: :: FLANG_3:3 for E being set for A being Subset of (E ^omega) for n, m being Nat st n <= m holds A |^ m c= A |^.. n proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for n, m being Nat st n <= m holds A |^ m c= A |^.. n let A be Subset of (E ^omega); ::_thesis: for n, m being Nat st n <= m holds A |^ m c= A |^.. n let n, m be Nat; ::_thesis: ( n <= m implies A |^ m c= A |^.. n ) assume n <= m ; ::_thesis: A |^ m c= A |^.. n then for x being set st x in A |^ m holds x in A |^.. n by Th2; hence A |^ m c= A |^.. n by TARSKI:def_3; ::_thesis: verum 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 = {} ) ) proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for n being Nat holds ( A |^.. n = {} iff ( n > 0 & A = {} ) ) let A be Subset of (E ^omega); ::_thesis: for n being Nat holds ( A |^.. n = {} iff ( n > 0 & A = {} ) ) let n be Nat; ::_thesis: ( A |^.. n = {} iff ( n > 0 & A = {} ) ) thus ( A |^.. n = {} implies ( n > 0 & A = {} ) ) ::_thesis: ( n > 0 & A = {} implies A |^.. n = {} ) proof A1: ( A <> {} implies A |^.. n <> {} ) proof assume A2: A <> {} ; ::_thesis: A |^.. n <> {} now__::_thesis:_for_m_being_Nat_holds_A_|^.._n_<>_{} let m be Nat; ::_thesis: A |^.. n <> {} consider m being Nat such that A3: n <= m ; A |^ m <> {} by A2, FLANG_1:27; then ex x being set st x in A |^ m by XBOOLE_0:def_1; hence A |^.. n <> {} by A3, Th2; ::_thesis: verum end; hence A |^.. n <> {} ; ::_thesis: verum end; assume that A4: A |^.. n = {} and A5: ( n <= 0 or A <> {} ) ; ::_thesis: contradiction ( n <= 0 implies <%> E in A |^.. n ) proof assume n <= 0 ; ::_thesis: <%> E in A |^.. n then A6: n = 0 ; A |^ 0 c= A |^.. 0 by Th3; then {(<%> E)} c= A |^.. 0 by FLANG_1:24; hence <%> E in A |^.. n by A6, ZFMISC_1:31; ::_thesis: verum end; hence contradiction by A4, A5, A1; ::_thesis: verum end; assume that A7: n > 0 and A8: A = {} ; ::_thesis: A |^.. n = {} now__::_thesis:_for_x_being_set_holds_not_x_in_A_|^.._n let x be set ; ::_thesis: not x in A |^.. n assume x in A |^.. n ; ::_thesis: contradiction then ex m being Nat st ( n <= m & x in A |^ m ) by Th2; hence contradiction by A7, A8, FLANG_1:27; ::_thesis: verum end; hence A |^.. n = {} by XBOOLE_0:def_1; ::_thesis: verum 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 proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for m, n being Nat st m <= n holds A |^.. n c= A |^.. m let A be Subset of (E ^omega); ::_thesis: for m, n being Nat st m <= n holds A |^.. n c= A |^.. m let m, n be Nat; ::_thesis: ( m <= n implies A |^.. n c= A |^.. m ) assume A1: m <= n ; ::_thesis: A |^.. n c= A |^.. m now__::_thesis:_for_x_being_set_st_x_in_A_|^.._n_holds_ x_in_A_|^.._m let x be set ; ::_thesis: ( x in A |^.. n implies x in A |^.. m ) assume x in A |^.. n ; ::_thesis: x in A |^.. m then consider k being Nat such that A2: n <= k and A3: x in A |^ k by Th2; m <= k by A1, A2, XXREAL_0:2; hence x in A |^.. m by A3, Th2; ::_thesis: verum end; hence A |^.. n c= A |^.. m by TARSKI:def_3; ::_thesis: verum 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 proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for k, m, n being Nat st k <= m holds A |^ (m,n) c= A |^.. k let A be Subset of (E ^omega); ::_thesis: for k, m, n being Nat st k <= m holds A |^ (m,n) c= A |^.. k let k, m, n be Nat; ::_thesis: ( k <= m implies A |^ (m,n) c= A |^.. k ) assume A1: k <= m ; ::_thesis: A |^ (m,n) c= A |^.. k now__::_thesis:_for_x_being_set_st_x_in_A_|^_(m,n)_holds_ x_in_A_|^.._k let x be set ; ::_thesis: ( x in A |^ (m,n) implies x in A |^.. k ) assume x in A |^ (m,n) ; ::_thesis: x in A |^.. k then consider l being Nat such that A2: m <= l and l <= n and A3: x in A |^ l by FLANG_2:19; k <= l by A1, A2, XXREAL_0:2; hence x in A |^.. k by A3, Th2; ::_thesis: verum end; hence A |^ (m,n) c= A |^.. k by TARSKI:def_3; ::_thesis: verum 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 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)) \/ (A |^.. (n + 1)) = A |^.. m let A be Subset of (E ^omega); ::_thesis: for m, n being Nat st m <= n + 1 holds (A |^ (m,n)) \/ (A |^.. (n + 1)) = A |^.. m let m, n be Nat; ::_thesis: ( m <= n + 1 implies (A |^ (m,n)) \/ (A |^.. (n + 1)) = A |^.. m ) assume m <= n + 1 ; ::_thesis: (A |^ (m,n)) \/ (A |^.. (n + 1)) = A |^.. m then A1: A |^.. (n + 1) c= A |^.. m by Th5; now__::_thesis:_for_x_being_set_st_x_in_A_|^.._m_holds_ x_in_(A_|^_(m,n))_\/_(A_|^.._(n_+_1)) let x be set ; ::_thesis: ( x in A |^.. m implies x in (A |^ (m,n)) \/ (A |^.. (n + 1)) ) assume x in A |^.. m ; ::_thesis: x in (A |^ (m,n)) \/ (A |^.. (n + 1)) then consider k being Nat such that A2: m <= k and A3: x in A |^ k by Th2; A4: now__::_thesis:_(_k_>_n_implies_x_in_A_|^.._(n_+_1)_) assume k > n ; ::_thesis: x in A |^.. (n + 1) then k >= n + 1 by NAT_1:13; hence x in A |^.. (n + 1) by A3, Th2; ::_thesis: verum end; ( k <= n implies x in A |^ (m,n) ) by A2, A3, FLANG_2:19; hence x in (A |^ (m,n)) \/ (A |^.. (n + 1)) by A4, XBOOLE_0:def_3; ::_thesis: verum end; then A5: A |^.. m c= (A |^ (m,n)) \/ (A |^.. (n + 1)) by TARSKI:def_3; A |^ (m,n) c= A |^.. m by Th6; then (A |^ (m,n)) \/ (A |^.. (n + 1)) c= A |^.. m by A1, XBOOLE_1:8; hence (A |^ (m,n)) \/ (A |^.. (n + 1)) = A |^.. m by A5, XBOOLE_0:def_10; ::_thesis: verum 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 proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for n being Nat holds (A |^ n) \/ (A |^.. (n + 1)) = A |^.. n let A be Subset of (E ^omega); ::_thesis: for n being Nat holds (A |^ n) \/ (A |^.. (n + 1)) = A |^.. n let n be Nat; ::_thesis: (A |^ n) \/ (A |^.. (n + 1)) = A |^.. n A1: n <= n + 1 by NAT_1:13; thus (A |^ n) \/ (A |^.. (n + 1)) = (A |^ (n,n)) \/ (A |^.. (n + 1)) by FLANG_2:22 .= A |^.. n by A1, Th7 ; ::_thesis: verum end; theorem Th9: :: FLANG_3:9 for E being set for A being Subset of (E ^omega) for n being Nat holds A |^.. n c= A * proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for n being Nat holds A |^.. n c= A * let A be Subset of (E ^omega); ::_thesis: for n being Nat holds A |^.. n c= A * let n be Nat; ::_thesis: A |^.. n c= A * now__::_thesis:_for_x_being_set_st_x_in_A_|^.._n_holds_ x_in_A_* let x be set ; ::_thesis: ( x in A |^.. n implies x in A * ) assume x in A |^.. n ; ::_thesis: x in A * then ex k being Nat st ( n <= k & x in A |^ k ) by Th2; hence x in A * by FLANG_1:41; ::_thesis: verum end; hence A |^.. n c= A * by TARSKI:def_3; ::_thesis: verum 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 ) ) 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 ) ::_thesis: ( ( n = 0 or <%> E in A ) implies <%> E in A |^.. n ) proof assume <%> E in A |^.. n ; ::_thesis: ( n = 0 or <%> E in A ) then A1: ex k being Nat st ( n <= k & <%> E in A |^ k ) by Th2; ( n = 0 or n > 0 ) ; hence ( n = 0 or <%> E in A ) by A1, FLANG_1:31; ::_thesis: verum end; assume A2: ( n = 0 or <%> E in A ) ; ::_thesis: <%> E in A |^.. n percases ( n = 0 or <%> E in A ) by A2; supposeA3: n = 0 ; ::_thesis: <%> E in A |^.. n {(<%> E)} = A |^ 0 by FLANG_1:24; then <%> E in A |^ n by A3, TARSKI:def_1; hence <%> E in A |^.. n by Th2; ::_thesis: verum end; suppose <%> E in A ; ::_thesis: <%> E in A |^.. n then <%> E in A |^ n by FLANG_1:30; hence <%> E in A |^.. n by Th2; ::_thesis: verum end; end; 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 ) ) proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for n being Nat holds ( A |^.. n = A * iff ( <%> E in A or n = 0 ) ) let A be Subset of (E ^omega); ::_thesis: for n being Nat holds ( A |^.. n = A * iff ( <%> E in A or n = 0 ) ) let n be Nat; ::_thesis: ( A |^.. n = A * iff ( <%> E in A or n = 0 ) ) thus ( not A |^.. n = A * or <%> E in A or n = 0 ) ::_thesis: ( ( <%> E in A or n = 0 ) implies A |^.. n = A * ) proof assume that A1: A |^.. n = A * and A2: not <%> E in A and A3: n <> 0 ; ::_thesis: contradiction <%> E in A * by FLANG_1:48; hence contradiction by A1, A2, A3, Th10; ::_thesis: verum end; assume A4: ( <%> E in A or n = 0 ) ; ::_thesis: A |^.. n = A * now__::_thesis:_for_x_being_set_st_x_in_A_*_holds_ x_in_A_|^.._n let x be set ; ::_thesis: ( x in A * implies b1 in A |^.. n ) assume x in A * ; ::_thesis: b1 in A |^.. n then consider k being Nat such that A5: x in A |^ k by FLANG_1:41; percases ( n <= k or k < n ) ; suppose n <= k ; ::_thesis: b1 in A |^.. n hence x in A |^.. n by A5, Th2; ::_thesis: verum end; suppose k < n ; ::_thesis: b1 in A |^.. n then A |^ k c= A |^ n by A4, FLANG_1:36; hence x in A |^.. n by A5, Th2; ::_thesis: verum end; end; end; then A6: A * c= A |^.. n by TARSKI:def_3; A |^.. n c= A * by Th9; hence A |^.. n = A * by A6, XBOOLE_0:def_10; ::_thesis: verum 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)) proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for n being Nat holds A * = (A |^ (0,n)) \/ (A |^.. (n + 1)) let A be Subset of (E ^omega); ::_thesis: for n being Nat holds A * = (A |^ (0,n)) \/ (A |^.. (n + 1)) let n be Nat; ::_thesis: A * = (A |^ (0,n)) \/ (A |^.. (n + 1)) thus A * = A |^.. 0 by Th11 .= (A |^ (0,n)) \/ (A |^.. (n + 1)) by Th7 ; ::_thesis: verum 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 proof let E be set ; ::_thesis: for A, B being Subset of (E ^omega) for n being Nat st A c= B holds A |^.. n c= B |^.. n let A, B be Subset of (E ^omega); ::_thesis: for n being Nat st A c= B holds A |^.. n c= B |^.. n let n be Nat; ::_thesis: ( A c= B implies A |^.. n c= B |^.. n ) assume A1: A c= B ; ::_thesis: A |^.. n c= B |^.. n now__::_thesis:_for_x_being_set_st_x_in_A_|^.._n_holds_ x_in_B_|^.._n let x be set ; ::_thesis: ( x in A |^.. n implies x in B |^.. n ) assume x in A |^.. n ; ::_thesis: x in B |^.. n then consider k being Nat such that A2: n <= k and A3: x in A |^ k by Th2; A |^ k c= B |^ k by A1, FLANG_1:37; hence x in B |^.. n by A2, A3, Th2; ::_thesis: verum end; hence A |^.. n c= B |^.. n by TARSKI:def_3; ::_thesis: verum end; theorem Th14: :: FLANG_3:14 for x, E being set for A being Subset of (E ^omega) for n being Nat st x in A & x <> <%> E 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 holds A |^.. n <> {(<%> E)} let A be Subset of (E ^omega); ::_thesis: for n being Nat st x in A & x <> <%> E holds A |^.. n <> {(<%> E)} let n be Nat; ::_thesis: ( x in A & x <> <%> E implies A |^.. n <> {(<%> E)} ) assume that A1: x in A and A2: x <> <%> E ; ::_thesis: A |^.. n <> {(<%> E)} percases ( n = 0 or n > 0 ) ; supposeA3: n = 0 ; ::_thesis: A |^.. n <> {(<%> E)} x in A |^ 1 by A1, FLANG_1:25; then x in A |^.. n by A3, Th2; hence A |^.. n <> {(<%> E)} by A2, TARSKI:def_1; ::_thesis: verum end; supposeA4: n > 0 ; ::_thesis: A |^.. n <> {(<%> E)} A5: A |^ n <> {} by A1, FLANG_1:27; A |^ n <> {(<%> E)} by A1, A2, A4, FLANG_2:7; then consider y being set such that A6: y in A |^ n and A7: y <> <%> E by A5, ZFMISC_1:35; y in A |^.. n by A6, Th2; hence A |^.. n <> {(<%> E)} by A7, TARSKI:def_1; ::_thesis: verum end; end; 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 = {} ) ) ) proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for n being Nat holds ( A |^.. n = {(<%> E)} iff ( A = {(<%> E)} or ( n = 0 & A = {} ) ) ) let A be Subset of (E ^omega); ::_thesis: for n being Nat holds ( A |^.. n = {(<%> E)} iff ( A = {(<%> E)} or ( n = 0 & A = {} ) ) ) let n be Nat; ::_thesis: ( A |^.. n = {(<%> E)} iff ( A = {(<%> E)} or ( n = 0 & A = {} ) ) ) thus ( not A |^.. n = {(<%> E)} or A = {(<%> E)} or ( n = 0 & A = {} ) ) ::_thesis: ( ( A = {(<%> E)} or ( n = 0 & A = {} ) ) implies A |^.. n = {(<%> E)} ) proof assume that A1: A |^.. n = {(<%> E)} and A2: A <> {(<%> E)} and A3: ( n <> 0 or A <> {} ) ; ::_thesis: contradiction percases ( n <> 0 or A <> {} ) by A3; supposeA4: n <> 0 ; ::_thesis: contradiction <%> E in A |^.. n by A1, ZFMISC_1:31; then consider k being Nat such that A5: n <= k and A6: <%> E in A |^ k by Th2; k > 0 by A4, A5; then A7: <%> E in A by A6, FLANG_1:31; for x being set holds ( not x in A or not x <> <%> E ) by A1, Th14; hence contradiction by A2, A7, ZFMISC_1:35; ::_thesis: verum end; suppose A <> {} ; ::_thesis: contradiction then ex x being set st ( x in A & x <> <%> E ) by A2, ZFMISC_1:35; hence contradiction by A1, Th14; ::_thesis: verum end; end; end; assume A8: ( A = {(<%> E)} or ( n = 0 & A = {} ) ) ; ::_thesis: A |^.. n = {(<%> E)} percases ( A = {(<%> E)} or ( n = 0 & A = {} ) ) by A8; supposeA9: A = {(<%> E)} ; ::_thesis: A |^.. n = {(<%> E)} A10: now__::_thesis:_for_x_being_set_st_x_in_{(<%>_E)}_holds_ x_in_A_|^.._n let x be set ; ::_thesis: ( x in {(<%> E)} implies x in A |^.. n ) assume x in {(<%> E)} ; ::_thesis: x in A |^.. n then x in A |^ n by A9, FLANG_1:28; hence x in A |^.. n by Th2; ::_thesis: verum end; now__::_thesis:_for_x_being_set_st_x_in_A_|^.._n_holds_ x_in_{(<%>_E)} let x be set ; ::_thesis: ( x in A |^.. n implies x in {(<%> E)} ) assume x in A |^.. n ; ::_thesis: x in {(<%> E)} then ex k being Nat st ( n <= k & x in A |^ k ) by Th2; hence x in {(<%> E)} by A9, FLANG_1:28; ::_thesis: verum end; hence A |^.. n = {(<%> E)} by A10, TARSKI:1; ::_thesis: verum end; supposeA11: ( n = 0 & A = {} ) ; ::_thesis: A |^.. n = {(<%> E)} hence A |^.. n = A * by Th11 .= {(<%> E)} by A11, FLANG_1:47 ; ::_thesis: verum end; end; 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 proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for n being Nat holds A |^.. (n + 1) = (A |^.. n) ^^ A let A be Subset of (E ^omega); ::_thesis: for n being Nat holds A |^.. (n + 1) = (A |^.. n) ^^ A let n be Nat; ::_thesis: A |^.. (n + 1) = (A |^.. n) ^^ A now__::_thesis:_for_x_being_set_st_x_in_A_|^.._(n_+_1)_holds_ x_in_(A_|^.._n)_^^_A let x be set ; ::_thesis: ( x in A |^.. (n + 1) implies x in (A |^.. n) ^^ A ) assume x in A |^.. (n + 1) ; ::_thesis: x in (A |^.. n) ^^ A then consider k being Nat such that A1: n + 1 <= k and A2: x in A |^ k by Th2; consider l being Nat such that A3: l + 1 = k by A1, NAT_1:6; x in (A |^ l) ^^ (A |^ 1) by A2, A3, FLANG_1:33; then consider a, b being Element of E ^omega such that A4: a in A |^ l and A5: b in A |^ 1 and A6: x = a ^ b by FLANG_1:def_1; n <= l by A1, A3, XREAL_1:6; then a in A |^.. n by A4, Th2; then x in (A |^.. n) ^^ (A |^ 1) by A5, A6, FLANG_1:def_1; hence x in (A |^.. n) ^^ A by FLANG_1:25; ::_thesis: verum end; then A7: A |^.. (n + 1) c= (A |^.. n) ^^ A by TARSKI:def_3; now__::_thesis:_for_x_being_set_st_x_in_(A_|^.._n)_^^_A_holds_ x_in_A_|^.._(n_+_1) let x be set ; ::_thesis: ( x in (A |^.. n) ^^ A implies x in A |^.. (n + 1) ) assume x in (A |^.. n) ^^ A ; ::_thesis: x in A |^.. (n + 1) then consider a, b being Element of E ^omega such that A8: a in A |^.. n and A9: b in A and A10: x = a ^ b by FLANG_1:def_1; consider k being Nat such that A11: n <= k and A12: a in A |^ k by A8, Th2; A13: n + 1 <= k + 1 by A11, XREAL_1:6; b in A |^ 1 by A9, FLANG_1:25; then x in A |^ (k + 1) by A10, A12, FLANG_1:40; hence x in A |^.. (n + 1) by A13, Th2; ::_thesis: verum end; then (A |^.. n) ^^ A c= A |^.. (n + 1) by TARSKI:def_3; hence A |^.. (n + 1) = (A |^.. n) ^^ A by A7, XBOOLE_0:def_10; ::_thesis: verum 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 proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for m being Nat holds (A |^.. m) ^^ (A *) = A |^.. m let A be Subset of (E ^omega); ::_thesis: for m being Nat holds (A |^.. m) ^^ (A *) = A |^.. m let m be Nat; ::_thesis: (A |^.. m) ^^ (A *) = A |^.. m now__::_thesis:_for_x_being_set_st_x_in_(A_|^.._m)_^^_(A_*)_holds_ x_in_A_|^.._m let x be set ; ::_thesis: ( x in (A |^.. m) ^^ (A *) implies x in A |^.. m ) assume x in (A |^.. m) ^^ (A *) ; ::_thesis: x in A |^.. m then consider a, b being Element of E ^omega such that A1: a in A |^.. m and A2: b in A * and A3: x = a ^ b by FLANG_1:def_1; consider k being Nat such that A4: b in A |^ k by A2, FLANG_1:41; consider l being Nat such that A5: m <= l and A6: a in A |^ l by A1, Th2; A7: l + k >= m by A5, NAT_1:12; a ^ b in A |^ (l + k) by A4, A6, FLANG_1:40; hence x in A |^.. m by A3, A7, Th2; ::_thesis: verum end; then A8: (A |^.. m) ^^ (A *) c= A |^.. m by TARSKI:def_3; <%> E in A * by FLANG_1:48; then A |^.. m c= (A |^.. m) ^^ (A *) by FLANG_1:16; hence (A |^.. m) ^^ (A *) = A |^.. m by A8, XBOOLE_0:def_10; ::_thesis: verum 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) proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for m, n being Nat holds (A |^.. m) ^^ (A |^.. n) = A |^.. (m + n) let A be Subset of (E ^omega); ::_thesis: for m, n being Nat holds (A |^.. m) ^^ (A |^.. n) = A |^.. (m + n) let m, n be Nat; ::_thesis: (A |^.. m) ^^ (A |^.. n) = A |^.. (m + n) defpred S1[ Nat] means (A |^.. m) ^^ (A |^.. $1) = A |^.. (m + $1); A1: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_ S1[n_+_1] let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A2: S1[n] ; ::_thesis: S1[n + 1] (A |^.. m) ^^ (A |^.. (n + 1)) = (A |^.. m) ^^ ((A |^.. n) ^^ A) by Th16 .= (A |^.. (m + n)) ^^ A by A2, FLANG_1:18 .= A |^.. ((m + n) + 1) by Th16 ; hence S1[n + 1] ; ::_thesis: verum end; (A |^.. m) ^^ (A |^.. 0) = (A |^.. m) ^^ (A *) by Th11 .= A |^.. (m + 0) by Th17 ; then A3: S1[ 0 ] ; for n being Nat holds S1[n] from NAT_1:sch_2(A3, A1); hence (A |^.. m) ^^ (A |^.. n) = A |^.. (m + n) ; ::_thesis: verum end; theorem Th19: :: FLANG_3:19 for E being set for A being Subset of (E ^omega) for n, m being Nat st n > 0 holds (A |^.. m) |^ n = A |^.. (m * n) proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for n, m being Nat st n > 0 holds (A |^.. m) |^ n = A |^.. (m * n) let A be Subset of (E ^omega); ::_thesis: for n, m being Nat st n > 0 holds (A |^.. m) |^ n = A |^.. (m * n) let n, m be Nat; ::_thesis: ( n > 0 implies (A |^.. m) |^ n = A |^.. (m * n) ) defpred S1[ Nat] means ( $1 > 0 implies (A |^.. m) |^ $1 = A |^.. (m * $1) ); A1: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_ S1[n_+_1] let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A2: S1[n] ; ::_thesis: S1[n + 1] now__::_thesis:_(_n_+_1_>_0_implies_(A_|^.._m)_|^_(n_+_1)_=_A_|^.._(m_*_(n_+_1))_) assume n + 1 > 0 ; ::_thesis: (A |^.. m) |^ (n + 1) = A |^.. (m * (n + 1)) percases ( n = 0 or n > 0 ) ; suppose n = 0 ; ::_thesis: (A |^.. m) |^ (n + 1) = A |^.. (m * (n + 1)) hence (A |^.. m) |^ (n + 1) = A |^.. (m * (n + 1)) by FLANG_1:25; ::_thesis: verum end; suppose n > 0 ; ::_thesis: (A |^.. m) |^ (n + 1) = A |^.. (m * (n + 1)) hence (A |^.. m) |^ (n + 1) = (A |^.. (m * n)) ^^ (A |^.. m) by A2, FLANG_1:23 .= A |^.. ((m * n) + m) by Th18 .= A |^.. (m * (n + 1)) ; ::_thesis: verum end; end; end; hence S1[n + 1] ; ::_thesis: verum end; A3: S1[ 0 ] ; for n being Nat holds S1[n] from NAT_1:sch_2(A3, A1); hence ( n > 0 implies (A |^.. m) |^ n = A |^.. (m * n) ) ; ::_thesis: verum end; theorem :: FLANG_3:20 for E being set for A being Subset of (E ^omega) for n being Nat holds (A |^.. n) * = (A |^.. n) ? proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for n being Nat holds (A |^.. n) * = (A |^.. n) ? let A be Subset of (E ^omega); ::_thesis: for n being Nat holds (A |^.. n) * = (A |^.. n) ? let n be Nat; ::_thesis: (A |^.. n) * = (A |^.. n) ? now__::_thesis:_for_x_being_set_st_x_in_(A_|^.._n)_*_holds_ x_in_(A_|^.._n)_? let x be set ; ::_thesis: ( x in (A |^.. n) * implies b1 in (A |^.. n) ? ) assume x in (A |^.. n) * ; ::_thesis: b1 in (A |^.. n) ? then consider k being Nat such that A1: x in (A |^.. n) |^ k by FLANG_1:41; percases ( k = 0 or k > 0 ) ; suppose k = 0 ; ::_thesis: b1 in (A |^.. n) ? then x in ((A |^.. n) |^ 0) \/ ((A |^.. n) |^ 1) by A1, XBOOLE_0:def_3; hence x in (A |^.. n) ? by FLANG_2:75; ::_thesis: verum end; supposeA2: k > 0 ; ::_thesis: b1 in (A |^.. n) ? then (A |^.. n) |^ k c= A |^.. (n * k) by Th19; then consider l being Nat such that A3: n * k <= l and A4: x in A |^ l by A1, Th2; k >= 0 + 1 by A2, NAT_1:13; then n * k >= n by XREAL_1:151; then l >= n by A3, XXREAL_0:2; then x in A |^.. n by A4, Th2; then x in (A |^.. n) |^ 1 by FLANG_1:25; then x in ((A |^.. n) |^ 0) \/ ((A |^.. n) |^ 1) by XBOOLE_0:def_3; hence x in (A |^.. n) ? by FLANG_2:75; ::_thesis: verum end; end; end; then A5: (A |^.. n) * c= (A |^.. n) ? by TARSKI:def_3; (A |^.. n) ? c= (A |^.. n) * by FLANG_2:86; hence (A |^.. n) * = (A |^.. n) ? by A5, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th21: :: FLANG_3:21 for E being set for A, C, B 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 let E be set ; ::_thesis: for A, C, B 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) let A, C, B be Subset of (E ^omega); ::_thesis: for m, n being Nat st A c= C |^.. m & B c= C |^.. n holds A ^^ B c= C |^.. (m + n) let m, n be Nat; ::_thesis: ( A c= C |^.. m & B c= C |^.. n implies A ^^ B c= C |^.. (m + n) ) assume that A1: A c= C |^.. m and A2: B c= C |^.. n ; ::_thesis: A ^^ B c= C |^.. (m + n) thus for x being set st x in A ^^ B holds x in C |^.. (m + n) :: according to TARSKI:def_3 ::_thesis: verum proof let x be set ; ::_thesis: ( x in A ^^ B implies x in C |^.. (m + n) ) assume x in A ^^ B ; ::_thesis: x in C |^.. (m + n) then consider a, b being Element of E ^omega such that A3: a in A and A4: b in B and A5: x = a ^ b by FLANG_1:def_1; a ^ b in (C |^.. m) ^^ (C |^.. n) by A1, A2, A3, A4, FLANG_1:def_1; hence x in C |^.. (m + n) by A5, Th18; ::_thesis: verum end; end; theorem Th22: :: FLANG_3:22 for E being set for A being Subset of (E ^omega) for n, k being Nat holds A |^.. (n + k) = (A |^.. n) ^^ (A |^ k) proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for n, k being Nat holds A |^.. (n + k) = (A |^.. n) ^^ (A |^ k) let A be Subset of (E ^omega); ::_thesis: for n, k being Nat holds A |^.. (n + k) = (A |^.. n) ^^ (A |^ k) let n, k be Nat; ::_thesis: A |^.. (n + k) = (A |^.. n) ^^ (A |^ k) defpred S1[ Nat] means A |^.. (n + $1) = (A |^.. n) ^^ (A |^ $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 |^.. (n + (k + 1)) = A |^.. ((n + k) + 1) .= ((A |^.. n) ^^ (A |^ k)) ^^ A by A2, Th16 .= (A |^.. n) ^^ ((A |^ k) ^^ A) by FLANG_1:18 .= (A |^.. n) ^^ (A |^ (k + 1)) by FLANG_1:23 ; hence S1[k + 1] ; ::_thesis: verum end; A |^.. (n + 0) = (A |^.. n) ^^ {(<%> E)} by FLANG_1:13 .= (A |^.. n) ^^ (A |^ 0) by FLANG_1:24 ; then A3: S1[ 0 ] ; for k being Nat holds S1[k] from NAT_1:sch_2(A3, A1); hence A |^.. (n + k) = (A |^.. n) ^^ (A |^ k) ; ::_thesis: verum 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 proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for n being Nat holds A ^^ (A |^.. n) = (A |^.. n) ^^ A let A be Subset of (E ^omega); ::_thesis: for n being Nat holds A ^^ (A |^.. n) = (A |^.. n) ^^ A let n be Nat; ::_thesis: A ^^ (A |^.. n) = (A |^.. n) ^^ A defpred S1[ Nat] means A ^^ (A |^.. $1) = (A |^.. $1) ^^ A; 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 ^^ (A |^.. (k + 1)) = A ^^ ((A |^.. k) ^^ A) by Th16 .= ((A |^.. k) ^^ A) ^^ A by A2, FLANG_1:18 .= (A |^.. (k + 1)) ^^ A by Th16 ; hence S1[k + 1] ; ::_thesis: verum end; A ^^ (A |^.. 0) = A ^^ (A *) by Th11 .= (A *) ^^ A by FLANG_1:57 .= (A |^.. 0) ^^ A by Th11 ; then A3: S1[ 0 ] ; for k being Nat holds S1[k] from NAT_1:sch_2(A3, A1); hence A ^^ (A |^.. n) = (A |^.. n) ^^ A ; ::_thesis: verum 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) proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for k, n being Nat holds (A |^ k) ^^ (A |^.. n) = (A |^.. n) ^^ (A |^ k) let A be Subset of (E ^omega); ::_thesis: for k, n being Nat holds (A |^ k) ^^ (A |^.. n) = (A |^.. n) ^^ (A |^ k) let k, n be Nat; ::_thesis: (A |^ k) ^^ (A |^.. n) = (A |^.. n) ^^ (A |^ k) defpred S1[ Nat] means (A |^ $1) ^^ (A |^.. n) = (A |^.. n) ^^ (A |^ $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 |^.. n) = ((A |^ k) ^^ A) ^^ (A |^.. n) by FLANG_1:23 .= (A ^^ (A |^ k)) ^^ (A |^.. n) by FLANG_1:32 .= A ^^ ((A |^.. n) ^^ (A |^ k)) by A2, FLANG_1:18 .= (A ^^ (A |^.. n)) ^^ (A |^ k) by FLANG_1:18 .= ((A |^.. n) ^^ A) ^^ (A |^ k) by Th23 .= (A |^.. n) ^^ (A ^^ (A |^ k)) by FLANG_1:18 .= (A |^.. n) ^^ ((A |^ k) ^^ A) by FLANG_1:32 .= (A |^.. n) ^^ (A |^ (k + 1)) by FLANG_1:23 ; hence S1[k + 1] ; ::_thesis: verum end; (A |^ 0) ^^ (A |^.. n) = {(<%> E)} ^^ (A |^.. n) by FLANG_1:24 .= A |^.. n by FLANG_1:13 .= (A |^.. n) ^^ {(<%> E)} by FLANG_1:13 .= (A |^.. n) ^^ (A |^ 0) by FLANG_1:24 ; then A3: S1[ 0 ] ; for k being Nat holds S1[k] from NAT_1:sch_2(A3, A1); hence (A |^ k) ^^ (A |^.. n) = (A |^.. n) ^^ (A |^ k) ; ::_thesis: verum 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)) proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for k, l, n being Nat holds (A |^ (k,l)) ^^ (A |^.. n) = (A |^.. n) ^^ (A |^ (k,l)) let A be Subset of (E ^omega); ::_thesis: for k, l, n being Nat holds (A |^ (k,l)) ^^ (A |^.. n) = (A |^.. n) ^^ (A |^ (k,l)) let k, l, n be Nat; ::_thesis: (A |^ (k,l)) ^^ (A |^.. n) = (A |^.. n) ^^ (A |^ (k,l)) defpred S1[ Nat] means (A |^ (k,l)) ^^ (A |^.. $1) = (A |^.. $1) ^^ (A |^ (k,l)); A1: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_ S1[n_+_1] let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A2: S1[n] ; ::_thesis: S1[n + 1] (A |^ (k,l)) ^^ (A |^.. (n + 1)) = (A |^ (k,l)) ^^ ((A |^.. n) ^^ A) by Th16 .= ((A |^.. n) ^^ (A |^ (k,l))) ^^ A by A2, FLANG_1:18 .= (A |^.. n) ^^ ((A |^ (k,l)) ^^ A) by FLANG_1:18 .= (A |^.. n) ^^ (A ^^ (A |^ (k,l))) by FLANG_2:36 .= ((A |^.. n) ^^ A) ^^ (A |^ (k,l)) by FLANG_1:18 .= (A |^.. (n + 1)) ^^ (A |^ (k,l)) by Th16 ; hence S1[n + 1] ; ::_thesis: verum end; (A |^ (k,l)) ^^ (A |^.. 0) = (A |^ (k,l)) ^^ (A *) by Th11 .= (A *) ^^ (A |^ (k,l)) by FLANG_2:66 .= (A |^.. 0) ^^ (A |^ (k,l)) by Th11 ; then A3: S1[ 0 ] ; for n being Nat holds S1[n] from NAT_1:sch_2(A3, A1); hence (A |^ (k,l)) ^^ (A |^.. n) = (A |^.. n) ^^ (A |^ (k,l)) ; ::_thesis: verum end; theorem :: FLANG_3:26 for E being set for B, A 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 let E be set ; ::_thesis: for B, A being Subset of (E ^omega) for n being Nat st <%> E in B holds ( A c= A ^^ (B |^.. n) & A c= (B |^.. n) ^^ A ) let B, A be Subset of (E ^omega); ::_thesis: for n being Nat st <%> E in B holds ( A c= A ^^ (B |^.. n) & A c= (B |^.. n) ^^ A ) let n be Nat; ::_thesis: ( <%> E in B implies ( A c= A ^^ (B |^.. n) & A c= (B |^.. n) ^^ A ) ) assume <%> E in B ; ::_thesis: ( A c= A ^^ (B |^.. n) & A c= (B |^.. n) ^^ A ) then <%> E in B |^.. n by Th10; hence ( A c= A ^^ (B |^.. n) & A c= (B |^.. n) ^^ A ) by FLANG_1:16; ::_thesis: verum 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) 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 Th18 .= (A |^.. n) ^^ (A |^.. m) by Th18 ; ::_thesis: verum 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 proof let E be set ; ::_thesis: 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 let A, B be Subset of (E ^omega); ::_thesis: for k, n being Nat st A c= B |^.. k & n > 0 holds A |^ n c= B |^.. k let k, n be Nat; ::_thesis: ( A c= B |^.. k & n > 0 implies A |^ n c= B |^.. k ) assume that A1: A c= B |^.. k and A2: n > 0 ; ::_thesis: A |^ n c= B |^.. k defpred S1[ Nat] means ( $1 > 0 implies A |^ $1 c= B |^.. k ); A3: now__::_thesis:_for_m_being_Nat_st_S1[m]_holds_ S1[m_+_1] let m be Nat; ::_thesis: ( S1[m] implies S1[b1 + 1] ) assume A4: S1[m] ; ::_thesis: S1[b1 + 1] percases ( m <= 0 or m > 0 ) ; suppose m <= 0 ; ::_thesis: S1[b1 + 1] then m = 0 ; hence S1[m + 1] by A1, FLANG_1:25; ::_thesis: verum end; suppose m > 0 ; ::_thesis: S1[b1 + 1] then (A |^ m) ^^ A c= (B |^.. k) ^^ (B |^.. k) by A1, A4, FLANG_1:17; then A |^ (m + 1) c= (B |^.. k) ^^ (B |^.. k) by FLANG_1:23; then A5: A |^ (m + 1) c= B |^.. (k + k) by Th18; B |^.. (k + k) c= B |^.. k by Th5, NAT_1:11; hence S1[m + 1] by A5, XBOOLE_1:1; ::_thesis: verum end; end; end; A6: S1[ 0 ] ; for m being Nat holds S1[m] from NAT_1:sch_2(A6, A3); hence A |^ n c= B |^.. k by A2; ::_thesis: verum 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 proof let E be set ; ::_thesis: 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 let A, B be Subset of (E ^omega); ::_thesis: for k, n being Nat st A c= B |^.. k & n > 0 holds A |^.. n c= B |^.. k let k, n be Nat; ::_thesis: ( A c= B |^.. k & n > 0 implies A |^.. n c= B |^.. k ) assume that A1: A c= B |^.. k and A2: n > 0 ; ::_thesis: A |^.. n c= B |^.. k let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A |^.. n or x in B |^.. k ) assume x in A |^.. n ; ::_thesis: x in B |^.. k then consider m being Nat such that A3: m >= n and A4: x in A |^ m by Th2; A |^ m c= B |^.. k by A1, A2, A3, Th28; hence x in B |^.. k by A4; ::_thesis: verum end; theorem Th30: :: FLANG_3:30 for E being set for A being Subset of (E ^omega) holds (A *) ^^ A = A |^.. 1 proof let E be set ; ::_thesis: for A being Subset of (E ^omega) holds (A *) ^^ A = A |^.. 1 let A be Subset of (E ^omega); ::_thesis: (A *) ^^ A = A |^.. 1 A1: now__::_thesis:_for_x_being_set_st_x_in_(A_*)_^^_A_holds_ x_in_A_|^.._1 let x be set ; ::_thesis: ( x in (A *) ^^ A implies x in A |^.. 1 ) assume x in (A *) ^^ A ; ::_thesis: x in A |^.. 1 then consider a1, a2 being Element of E ^omega such that A2: a1 in A * and A3: a2 in A and A4: x = a1 ^ a2 by FLANG_1:def_1; consider n being Nat such that A5: a1 in A |^ n by A2, FLANG_1:41; A6: n + 1 >= 1 by NAT_1:11; a2 in A |^ 1 by A3, FLANG_1:25; then a1 ^ a2 in A |^ (n + 1) by A5, FLANG_1:40; hence x in A |^.. 1 by A4, A6, Th2; ::_thesis: verum end; now__::_thesis:_for_x_being_set_st_x_in_A_|^.._1_holds_ x_in_(A_*)_^^_A let x be set ; ::_thesis: ( x in A |^.. 1 implies x in (A *) ^^ A ) assume x in A |^.. 1 ; ::_thesis: x in (A *) ^^ A then consider n being Nat such that A7: n >= 1 and A8: x in A |^ n by Th2; consider m being Nat such that A9: m + 1 = n by A7, NAT_1:6; A |^ (m + 1) c= (A *) ^^ A by FLANG_1:51; hence x in (A *) ^^ A by A8, A9; ::_thesis: verum end; hence (A *) ^^ A = A |^.. 1 by A1, TARSKI:1; ::_thesis: verum end; theorem :: FLANG_3:31 for E being set for A being Subset of (E ^omega) for k being Nat holds (A *) ^^ (A |^ k) = A |^.. k proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for k being Nat holds (A *) ^^ (A |^ k) = A |^.. k let A be Subset of (E ^omega); ::_thesis: for k being Nat holds (A *) ^^ (A |^ k) = A |^.. k let k be Nat; ::_thesis: (A *) ^^ (A |^ k) = A |^.. k defpred S1[ Nat] means (A *) ^^ (A |^ $1) = A |^.. $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 *) ^^ (A |^ (k + 1)) = (A *) ^^ ((A |^ k) ^^ A) by FLANG_1:23 .= (A |^.. k) ^^ A by A2, FLANG_1:18 .= A |^.. (k + 1) by Th16 ; hence S1[k + 1] ; ::_thesis: verum end; (A *) ^^ (A |^ 0) = (A *) ^^ {(<%> E)} by FLANG_1:24 .= A * by FLANG_1:13 .= A |^.. 0 by Th11 ; then A3: S1[ 0 ] ; for k being Nat holds S1[k] from NAT_1:sch_2(A3, A1); hence (A *) ^^ (A |^ k) = A |^.. k ; ::_thesis: verum 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) proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for m being Nat holds (A |^.. m) ^^ (A *) = (A *) ^^ (A |^.. m) let A be Subset of (E ^omega); ::_thesis: for m being Nat holds (A |^.. m) ^^ (A *) = (A *) ^^ (A |^.. m) let m be Nat; ::_thesis: (A |^.. m) ^^ (A *) = (A *) ^^ (A |^.. m) thus (A |^.. m) ^^ (A *) = (A |^.. m) ^^ (A |^.. 0) by Th11 .= (A |^.. 0) ^^ (A |^.. m) by Th27 .= (A *) ^^ (A |^.. m) by Th11 ; ::_thesis: verum 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) proof let E be set ; ::_thesis: 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) let A be Subset of (E ^omega); ::_thesis: for k, l, n being Nat st k <= l holds (A |^.. n) ^^ (A |^ (k,l)) = A |^.. (n + k) let k, l, n be Nat; ::_thesis: ( k <= l implies (A |^.. n) ^^ (A |^ (k,l)) = A |^.. (n + k) ) assume A1: k <= l ; ::_thesis: (A |^.. n) ^^ (A |^ (k,l)) = A |^.. (n + k) A2: A |^.. (n + k) c= (A |^.. n) ^^ (A |^ (k,l)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A |^.. (n + k) or x in (A |^.. n) ^^ (A |^ (k,l)) ) assume x in A |^.. (n + k) ; ::_thesis: x in (A |^.. n) ^^ (A |^ (k,l)) then consider i being Nat such that A3: i >= n + k and A4: x in A |^ i by Th2; consider m being Nat such that A5: (n + k) + m = i by A3, NAT_1:10; i = (n + m) + k by A5; then x in (A |^ (n + m)) ^^ (A |^ k) by A4, FLANG_1:33; then A6: ex a, b being Element of E ^omega st ( a in A |^ (n + m) & b in A |^ k & x = a ^ b ) by FLANG_1:def_1; A7: A |^ (n + m) c= A |^.. n by Th3, NAT_1:11; A |^ k c= A |^ (k,l) by A1, FLANG_2:20; hence x in (A |^.. n) ^^ (A |^ (k,l)) by A6, A7, FLANG_1:def_1; ::_thesis: verum end; (A |^.. n) ^^ (A |^ (k,l)) c= A |^.. (n + k) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A |^.. n) ^^ (A |^ (k,l)) or x in A |^.. (n + k) ) assume x in (A |^.. n) ^^ (A |^ (k,l)) ; ::_thesis: x in A |^.. (n + k) then consider a, b being Element of E ^omega such that A8: a in A |^.. n and A9: b in A |^ (k,l) and A10: x = a ^ b by FLANG_1:def_1; A |^ (k,l) c= A |^.. k by Th6; then a ^ b in (A |^.. n) ^^ (A |^.. k) by A8, A9, FLANG_1:def_1; hence x in A |^.. (n + k) by A10, Th18; ::_thesis: verum end; hence (A |^.. n) ^^ (A |^ (k,l)) = A |^.. (n + k) by A2, XBOOLE_0:def_10; ::_thesis: verum 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 proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for k, l being Nat st k <= l holds (A *) ^^ (A |^ (k,l)) = A |^.. k let A be Subset of (E ^omega); ::_thesis: for k, l being Nat st k <= l holds (A *) ^^ (A |^ (k,l)) = A |^.. k let k, l be Nat; ::_thesis: ( k <= l implies (A *) ^^ (A |^ (k,l)) = A |^.. k ) assume k <= l ; ::_thesis: (A *) ^^ (A |^ (k,l)) = A |^.. k then (A |^.. 0) ^^ (A |^ (k,l)) = A |^.. (0 + k) by Th33; hence (A *) ^^ (A |^ (k,l)) = A |^.. k by Th11; ::_thesis: verum 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) proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for m, n being Nat holds (A |^ m) |^.. n c= A |^.. (m * n) let A be Subset of (E ^omega); ::_thesis: for m, n being Nat holds (A |^ m) |^.. n c= A |^.. (m * n) let m, n be Nat; ::_thesis: (A |^ m) |^.. n c= A |^.. (m * n) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A |^ m) |^.. n or x in A |^.. (m * n) ) assume x in (A |^ m) |^.. n ; ::_thesis: x in A |^.. (m * n) then consider k being Nat such that A1: k >= n and A2: x in (A |^ m) |^ k by Th2; A3: m * k >= m * n by A1, XREAL_1:64; x in A |^ (m * k) by A2, FLANG_1:34; hence x in A |^.. (m * n) by A3, Th2; ::_thesis: verum 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 proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for m, n being Nat holds (A |^ m) |^.. n c= (A |^.. n) |^ m let A be Subset of (E ^omega); ::_thesis: for m, n being Nat holds (A |^ m) |^.. n c= (A |^.. n) |^ m let m, n be Nat; ::_thesis: (A |^ m) |^.. n c= (A |^.. n) |^ m percases ( m > 0 or m <= 0 ) ; supposeA1: m > 0 ; ::_thesis: (A |^ m) |^.. n c= (A |^.. n) |^ m (A |^ m) |^.. n c= A |^.. (m * n) by Th35; hence (A |^ m) |^.. n c= (A |^.. n) |^ m by A1, Th19; ::_thesis: verum end; suppose m <= 0 ; ::_thesis: (A |^ m) |^.. n c= (A |^.. n) |^ m then A2: m = 0 ; then (A |^ m) |^.. n = {(<%> E)} |^.. n by FLANG_1:24 .= {(<%> E)} by Th15 .= (A |^.. n) |^ m by A2, FLANG_1:24 ; hence (A |^ m) |^.. n c= (A |^.. n) |^ m ; ::_thesis: verum end; end; 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) proof let E be set ; ::_thesis: 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) let C be Subset of (E ^omega); ::_thesis: 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) let a, b be Element of E ^omega ; ::_thesis: for m, n being Nat st a in C |^.. m & b in C |^.. n holds a ^ b in C |^.. (m + n) let m, n be Nat; ::_thesis: ( a in C |^.. m & b in C |^.. n implies a ^ b in C |^.. (m + n) ) assume that A1: a in C |^.. m and A2: b in C |^.. n ; ::_thesis: a ^ b in C |^.. (m + n) A3: (C |^.. m) ^^ (C |^.. n) c= C |^.. (m + n) by Th21; a ^ b in (C |^.. m) ^^ (C |^.. n) by A1, A2, FLANG_1:def_1; hence a ^ b in C |^.. (m + n) by A3; ::_thesis: verum end; theorem Th38: :: FLANG_3:38 for x, E being set for A being Subset of (E ^omega) for k being Nat st A |^.. k = {x} holds x = <%> E proof let x, E be set ; ::_thesis: for A being Subset of (E ^omega) for k being Nat st A |^.. k = {x} holds x = <%> E let A be Subset of (E ^omega); ::_thesis: for k being Nat st A |^.. k = {x} holds x = <%> E let k be Nat; ::_thesis: ( A |^.. k = {x} implies x = <%> E ) assume that A1: A |^.. k = {x} and A2: x <> <%> E ; ::_thesis: contradiction reconsider a = x as Element of E ^omega by A1, ZFMISC_1:31; x in A |^.. k by A1, ZFMISC_1:31; then A3: a ^ a in A |^.. (k + k) by Th37; A4: A |^.. (k + k) c= A |^.. k by Th5, NAT_1:11; a ^ a <> x by A2, FLANG_1:11; hence contradiction by A1, A4, A3, TARSKI:def_1; ::_thesis: verum 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 * proof let E be set ; ::_thesis: for A, B being Subset of (E ^omega) for n being Nat st A c= B * holds A |^.. n c= B * let A, B be Subset of (E ^omega); ::_thesis: for n being Nat st A c= B * holds A |^.. n c= B * let n be Nat; ::_thesis: ( A c= B * implies A |^.. n c= B * ) assume A1: A c= B * ; ::_thesis: A |^.. n c= B * let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A |^.. n or x in B * ) assume x in A |^.. n ; ::_thesis: x in B * then consider k being Nat such that k >= n and A2: x in A |^ k by Th2; A |^ k c= B * by A1, FLANG_1:59; hence x in B * by A2; ::_thesis: verum 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 ) ) proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for k being Nat holds ( A ? c= A |^.. k iff ( k = 0 or <%> E in A ) ) let A be Subset of (E ^omega); ::_thesis: for k being Nat holds ( A ? c= A |^.. k iff ( k = 0 or <%> E in A ) ) let k be Nat; ::_thesis: ( A ? c= A |^.. k iff ( k = 0 or <%> E in A ) ) thus ( not A ? c= A |^.. k or k = 0 or <%> E in A ) ::_thesis: ( ( k = 0 or <%> E in A ) implies A ? c= A |^.. k ) proof A1: <%> E in A ? by FLANG_2:78; assume A ? c= A |^.. k ; ::_thesis: ( k = 0 or <%> E in A ) hence ( k = 0 or <%> E in A ) by A1, Th10; ::_thesis: verum end; assume ( k = 0 or <%> E in A ) ; ::_thesis: A ? c= A |^.. k then A |^.. k = A * by Th11; hence A ? c= A |^.. k by FLANG_2:86; ::_thesis: verum 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 proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for k being Nat holds (A |^.. k) ^^ (A ?) = A |^.. k let A be Subset of (E ^omega); ::_thesis: for k being Nat holds (A |^.. k) ^^ (A ?) = A |^.. k let k be Nat; ::_thesis: (A |^.. k) ^^ (A ?) = A |^.. k thus (A |^.. k) ^^ (A ?) = (A |^.. k) ^^ (A |^ (0,1)) by FLANG_2:79 .= A |^.. (k + 0) by Th33 .= A |^.. k ; ::_thesis: verum 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) proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for k being Nat holds (A |^.. k) ^^ (A ?) = (A ?) ^^ (A |^.. k) let A be Subset of (E ^omega); ::_thesis: for k being Nat holds (A |^.. k) ^^ (A ?) = (A ?) ^^ (A |^.. k) let k be Nat; ::_thesis: (A |^.. k) ^^ (A ?) = (A ?) ^^ (A |^.. k) thus (A |^.. k) ^^ (A ?) = (A |^.. k) ^^ (A |^ (0,1)) by FLANG_2:79 .= (A |^ (0,1)) ^^ (A |^.. k) by Th25 .= (A ?) ^^ (A |^.. k) by FLANG_2:79 ; ::_thesis: verum end; theorem :: FLANG_3:43 for E being set for B, A 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 let E be set ; ::_thesis: for B, A 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 ) let B, A be Subset of (E ^omega); ::_thesis: for k being Nat st B c= A * holds ( (A |^.. k) ^^ B c= A |^.. k & B ^^ (A |^.. k) c= A |^.. k ) let k be Nat; ::_thesis: ( B c= A * implies ( (A |^.. k) ^^ B c= A |^.. k & B ^^ (A |^.. k) c= A |^.. k ) ) assume A1: B c= A * ; ::_thesis: ( (A |^.. k) ^^ B c= A |^.. k & B ^^ (A |^.. k) c= A |^.. k ) then B ^^ (A |^.. k) c= (A *) ^^ (A |^.. k) by FLANG_1:17; then A2: B ^^ (A |^.. k) c= (A |^.. k) ^^ (A *) by Th32; (A |^.. k) ^^ B c= (A |^.. k) ^^ (A *) by A1, FLANG_1:17; hence ( (A |^.. k) ^^ B c= A |^.. k & B ^^ (A |^.. k) c= A |^.. k ) by A2, Th17; ::_thesis: verum 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) proof let E be set ; ::_thesis: for A, B being Subset of (E ^omega) for k being Nat holds (A /\ B) |^.. k c= (A |^.. k) /\ (B |^.. k) let A, B be Subset of (E ^omega); ::_thesis: for k being Nat holds (A /\ B) |^.. k c= (A |^.. k) /\ (B |^.. k) let k be Nat; ::_thesis: (A /\ B) |^.. k c= (A |^.. k) /\ (B |^.. k) thus for x being set st x in (A /\ B) |^.. k holds x in (A |^.. k) /\ (B |^.. k) :: according to TARSKI:def_3 ::_thesis: verum proof let x be set ; ::_thesis: ( x in (A /\ B) |^.. k implies x in (A |^.. k) /\ (B |^.. k) ) assume x in (A /\ B) |^.. k ; ::_thesis: x in (A |^.. k) /\ (B |^.. k) then consider m being Nat such that A1: k <= m and A2: x in (A /\ B) |^ m by Th2; A3: B |^ m c= B |^.. k by A1, Th3; (A /\ B) |^ m c= (A |^ m) /\ (B |^ m) by FLANG_1:39; then A4: x in (A |^ m) /\ (B |^ m) by A2; A |^ m c= A |^.. k by A1, Th3; then (A |^ m) /\ (B |^ m) c= (A |^.. k) /\ (B |^.. k) by A3, XBOOLE_1:27; hence x in (A |^.. k) /\ (B |^.. k) by A4; ::_thesis: verum end; 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 proof let E be set ; ::_thesis: for A, B being Subset of (E ^omega) for k being Nat holds (A |^.. k) \/ (B |^.. k) c= (A \/ B) |^.. k let A, B be Subset of (E ^omega); ::_thesis: for k being Nat holds (A |^.. k) \/ (B |^.. k) c= (A \/ B) |^.. k let k be Nat; ::_thesis: (A |^.. k) \/ (B |^.. k) c= (A \/ B) |^.. k thus for x being set st x in (A |^.. k) \/ (B |^.. k) holds x in (A \/ B) |^.. k :: according to TARSKI:def_3 ::_thesis: verum proof let x be set ; ::_thesis: ( x in (A |^.. k) \/ (B |^.. k) implies x in (A \/ B) |^.. k ) assume A1: x in (A |^.. k) \/ (B |^.. k) ; ::_thesis: x in (A \/ B) |^.. k percases ( x in A |^.. k or x in B |^.. k ) by A1, XBOOLE_0:def_3; suppose x in A |^.. k ; ::_thesis: x in (A \/ B) |^.. k then consider m being Nat such that A2: k <= m and A3: x in A |^ m by Th2; A4: (A |^ m) \/ (B |^ m) c= (A \/ B) |^ m by FLANG_1:38; A |^ m c= (A |^ m) \/ (B |^ m) by XBOOLE_1:7; then A |^ m c= (A \/ B) |^ m by A4, XBOOLE_1:1; then A5: x in (A \/ B) |^ m by A3; (A \/ B) |^ m c= (A \/ B) |^.. k by A2, Th3; hence x in (A \/ B) |^.. k by A5; ::_thesis: verum end; suppose x in B |^.. k ; ::_thesis: x in (A \/ B) |^.. k then consider m being Nat such that A6: k <= m and A7: x in B |^ m by Th2; A8: (A |^ m) \/ (B |^ m) c= (A \/ B) |^ m by FLANG_1:38; B |^ m c= (A |^ m) \/ (B |^ m) by XBOOLE_1:7; then B |^ m c= (A \/ B) |^ m by A8, XBOOLE_1:1; then A9: x in (A \/ B) |^ m by A7; (A \/ B) |^ m c= (A \/ B) |^.. k by A6, Th3; hence x in (A \/ B) |^.. k by A9; ::_thesis: verum end; end; end; end; theorem Th46: :: FLANG_3:46 for x, E 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 ) ) ) proof let x, E be set ; ::_thesis: 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 ) ) ) let A be Subset of (E ^omega); ::_thesis: for k being Nat holds ( <%x%> in A |^.. k iff ( <%x%> in A & ( <%> E in A or k <= 1 ) ) ) let k be Nat; ::_thesis: ( <%x%> in A |^.. k iff ( <%x%> in A & ( <%> E in A or k <= 1 ) ) ) thus ( <%x%> in A |^.. k implies ( <%x%> in A & ( <%> E in A or k <= 1 ) ) ) ::_thesis: ( <%x%> in A & ( <%> E in A or k <= 1 ) implies <%x%> in A |^.. k ) proof assume <%x%> in A |^.. k ; ::_thesis: ( <%x%> in A & ( <%> E in A or k <= 1 ) ) then ex m being Nat st ( k <= m & <%x%> in A |^ m ) by Th2; hence ( <%x%> in A & ( <%> E in A or k <= 1 ) ) by FLANG_2:9; ::_thesis: verum end; assume that A1: <%x%> in A and A2: ( <%> E in A or k <= 1 ) ; ::_thesis: <%x%> in A |^.. k percases ( ( <%> E in A & k > 1 ) or k = 0 or k = 1 ) by A2, NAT_1:25; suppose ( <%> E in A & k > 1 ) ; ::_thesis: <%x%> in A |^.. k then <%x%> in A |^ k by A1, FLANG_2:9; hence <%x%> in A |^.. k by Th2; ::_thesis: verum end; suppose k = 0 ; ::_thesis: <%x%> in A |^.. k then A |^.. k = A * by Th11; hence <%x%> in A |^.. k by A1, FLANG_1:72; ::_thesis: verum end; suppose k = 1 ; ::_thesis: <%x%> in A |^.. k then <%x%> in A |^ k by A1, FLANG_1:25; hence <%x%> in A |^.. k by Th2; ::_thesis: verum end; end; 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 proof let E be set ; ::_thesis: for A, B being Subset of (E ^omega) for k being Nat st A c= B |^.. k holds B |^.. k = (B \/ A) |^.. k let A, B be Subset of (E ^omega); ::_thesis: for k being Nat st A c= B |^.. k holds B |^.. k = (B \/ A) |^.. k let k be Nat; ::_thesis: ( A c= B |^.. k implies B |^.. k = (B \/ A) |^.. k ) defpred S1[ Nat] means ( $1 >= k implies (B \/ A) |^ $1 c= B |^.. k ); B |^ 1 c= B |^.. 1 by Th3; then A1: B c= B |^.. 1 by FLANG_1:25; assume A2: A c= B |^.. k ; ::_thesis: B |^.. k = (B \/ A) |^.. k A3: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_ S1[n_+_1] let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A4: S1[n] ; ::_thesis: S1[n + 1] now__::_thesis:_(_n_+_1_>=_k_implies_(B_\/_A)_|^_(n_+_1)_c=_B_|^.._k_) assume A5: n + 1 >= k ; ::_thesis: (B \/ A) |^ (n + 1) c= B |^.. k percases ( n + 1 = k or n >= k ) by A5, NAT_1:8; supposeA6: n + 1 = k ; ::_thesis: (B \/ A) |^ (n + 1) c= B |^.. k percases ( k = 0 or k > 0 ) ; suppose k = 0 ; ::_thesis: (B \/ A) |^ (n + 1) c= B |^.. k hence (B \/ A) |^ (n + 1) c= B |^.. k by A6; ::_thesis: verum end; supposeA7: k > 0 ; ::_thesis: (B \/ A) |^ (n + 1) c= B |^.. k then k >= 0 + 1 by NAT_1:13; then B |^.. k c= B |^.. 1 by Th5; then A c= B |^.. 1 by A2, XBOOLE_1:1; then B \/ A c= B |^.. 1 by A1, XBOOLE_1:8; then A8: (B \/ A) |^ k c= (B |^.. 1) |^ k by FLANG_1:37; (B |^.. 1) |^ k c= B |^.. (1 * k) by A7, Th19; hence (B \/ A) |^ (n + 1) c= B |^.. k by A6, A8, XBOOLE_1:1; ::_thesis: verum end; end; end; supposeA9: n >= k ; ::_thesis: (B \/ A) |^ (n + 1) c= B |^.. k A10: B |^.. (k + k) c= B |^.. k by Th5, NAT_1:11; ((B \/ A) |^ n) ^^ A c= B |^.. (k + k) by A2, A4, A9, Th21; then A11: ((B \/ A) |^ n) ^^ A c= B |^.. k by A10, XBOOLE_1:1; A12: B |^.. (k + 1) c= B |^.. k by Th5, NAT_1:11; ((B \/ A) |^ n) ^^ B c= B |^.. (k + 1) by A1, A4, A9, Th21; then A13: ((B \/ A) |^ n) ^^ B c= B |^.. k by A12, XBOOLE_1:1; (B \/ A) |^ (n + 1) = ((B \/ A) |^ n) ^^ (B \/ A) by FLANG_1:23 .= (((B \/ A) |^ n) ^^ B) \/ (((B \/ A) |^ n) ^^ A) by FLANG_1:20 ; hence (B \/ A) |^ (n + 1) c= B |^.. k by A13, A11, XBOOLE_1:8; ::_thesis: verum end; end; end; hence S1[n + 1] ; ::_thesis: verum end; A14: S1[ 0 ] proof assume 0 >= k ; ::_thesis: (B \/ A) |^ 0 c= B |^.. k then k = 0 ; then A15: B |^.. k = B * by Th11; A16: <%> E in B * by FLANG_1:48; (B \/ A) |^ 0 = {(<%> E)} by FLANG_1:24; hence (B \/ A) |^ 0 c= B |^.. k by A15, A16, ZFMISC_1:31; ::_thesis: verum end; A17: for n being Nat holds S1[n] from NAT_1:sch_2(A14, A3); A18: (B \/ A) |^.. k c= B |^.. k proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (B \/ A) |^.. k or x in B |^.. k ) assume x in (B \/ A) |^.. k ; ::_thesis: x in B |^.. k then consider n being Nat such that A19: n >= k and A20: x in (B \/ A) |^ n by Th2; (B \/ A) |^ n c= B |^.. k by A17, A19; hence x in B |^.. k by A20; ::_thesis: verum end; B |^.. k c= (B \/ A) |^.. k by Th13, XBOOLE_1:7; hence B |^.. k = (B \/ A) |^.. k by A18, XBOOLE_0:def_10; ::_thesis: verum end; begin definition let E be set ; let A be Subset of (E ^omega); funcA + -> 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 ) } is Subset of (E ^omega) proof defpred S1[ set ] means ex n being Nat st ( n > 0 & $1 = A |^ n ); 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 n being Nat st ( n > 0 & B = A |^ n ) } is Subset of (E ^omega) ; ::_thesis: verum end; 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 ) } ; 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 ) ) proof let E, x be set ; ::_thesis: for A being Subset of (E ^omega) holds ( x in A + iff ex n being Nat st ( n > 0 & x in A |^ n ) ) let A be Subset of (E ^omega); ::_thesis: ( x in A + iff ex n being Nat st ( n > 0 & x in A |^ n ) ) thus ( x in A + implies ex n being Nat st ( n > 0 & x in A |^ n ) ) ::_thesis: ( ex n being Nat st ( n > 0 & x in A |^ n ) implies x in A + ) proof defpred S1[ set ] means ex n being Nat st ( n > 0 & $1 = A |^ n ); assume x in A + ; ::_thesis: ex n being Nat st ( n > 0 & x in A |^ n ) then consider X being set such that A1: x in X and A2: X in { B where B is Subset of (E ^omega) : ex n being Nat st ( n > 0 & B = A |^ n ) } 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 n being Nat st ( n > 0 & x in A |^ n ) by A1; ::_thesis: verum end; given n being Nat such that A4: n > 0 and A5: x in A |^ n ; ::_thesis: x in A + defpred S1[ set ] means ex n being Nat st ( n > 0 & $1 = A |^ n ); consider B being Subset of (E ^omega) such that A6: x in B and A7: S1[B] by A4, A5; 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 A7; hence x in A + by A6, TARSKI:def_4; ::_thesis: verum end; theorem Th49: :: FLANG_3:49 for E being set for A being Subset of (E ^omega) for n being Nat st n > 0 holds A |^ n c= A + proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for n being Nat st n > 0 holds A |^ n c= A + let A be Subset of (E ^omega); ::_thesis: for n being Nat st n > 0 holds A |^ n c= A + let n be Nat; ::_thesis: ( n > 0 implies A |^ n c= A + ) assume n > 0 ; ::_thesis: A |^ n c= A + then for x being set st x in A |^ n holds x in A + by Th48; hence A |^ n c= A + by TARSKI:def_3; ::_thesis: verum end; theorem Th50: :: FLANG_3:50 for E being set for A being Subset of (E ^omega) holds A + = A |^.. 1 proof let E be set ; ::_thesis: for A being Subset of (E ^omega) holds A + = A |^.. 1 let A be Subset of (E ^omega); ::_thesis: A + = A |^.. 1 A1: now__::_thesis:_for_x_being_set_st_x_in_A_+_holds_ x_in_A_|^.._1 let x be set ; ::_thesis: ( x in A + implies x in A |^.. 1 ) assume x in A + ; ::_thesis: x in A |^.. 1 then consider k being Nat such that A2: 0 < k and A3: x in A |^ k by Th48; 0 + 1 <= k by A2, NAT_1:13; hence x in A |^.. 1 by A3, Th2; ::_thesis: verum end; now__::_thesis:_for_x_being_set_st_x_in_A_|^.._1_holds_ x_in_A_+ let x be set ; ::_thesis: ( x in A |^.. 1 implies x in A + ) assume x in A |^.. 1 ; ::_thesis: x in A + then ex k being Nat st ( 1 <= k & x in A |^ k ) by Th2; hence x in A + by Th48; ::_thesis: verum end; hence A + = A |^.. 1 by A1, TARSKI:1; ::_thesis: verum end; theorem :: FLANG_3:51 for E being set for A being Subset of (E ^omega) holds ( A + = {} iff A = {} ) proof let E be set ; ::_thesis: for A being Subset of (E ^omega) holds ( A + = {} iff A = {} ) let A be Subset of (E ^omega); ::_thesis: ( A + = {} iff A = {} ) A + = A |^.. 1 by Th50; hence ( A + = {} iff A = {} ) by Th4; ::_thesis: verum end; theorem Th52: :: FLANG_3:52 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 (A *) ^^ A = A |^.. 1 by Th30; hence A + = (A *) ^^ A by Th50; ::_thesis: verum end; theorem Th53: :: FLANG_3:53 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 +) thus A * = {(<%> E)} \/ ((A *) ^^ A) by FLANG_1:56 .= {(<%> E)} \/ (A +) by Th52 ; ::_thesis: verum 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)) proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for n being Nat holds A + = (A |^ (1,n)) \/ (A |^.. (n + 1)) let A be Subset of (E ^omega); ::_thesis: for n being Nat holds A + = (A |^ (1,n)) \/ (A |^.. (n + 1)) let n be Nat; ::_thesis: A + = (A |^ (1,n)) \/ (A |^.. (n + 1)) A1: 0 + 1 <= n + 1 by XREAL_1:7; thus A + = A |^.. 1 by Th50 .= (A |^ (1,n)) \/ (A |^.. (n + 1)) by A1, Th7 ; ::_thesis: verum end; theorem Th55: :: FLANG_3:55 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 |^.. 1 c= A * by Th9; hence A + c= A * by Th50; ::_thesis: verum end; theorem Th56: :: FLANG_3:56 for E being set for A being Subset of (E ^omega) holds ( <%> E in A + iff <%> E in A ) proof let E be set ; ::_thesis: for A being Subset of (E ^omega) holds ( <%> E in A + iff <%> E in A ) let A be Subset of (E ^omega); ::_thesis: ( <%> E in A + iff <%> E in A ) A + = A |^.. 1 by Th50; hence ( <%> E in A + iff <%> E in A ) by Th10; ::_thesis: verum end; theorem Th57: :: FLANG_3:57 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 <%> E in A + by FLANG_1:48; hence <%> E in A by Th56; ::_thesis: verum end; assume <%> E in A ; ::_thesis: A + = A * then A * = (A *) ^^ A by FLANG_1:54; hence A + = A * by Th52; ::_thesis: verum end; theorem Th58: :: FLANG_3:58 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 |^.. 1 c= B |^.. 1 by Th13; then A + c= B |^.. 1 by Th50; hence A + c= B + by Th50; ::_thesis: verum end; theorem Th59: :: FLANG_3:59 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 |^ 1 c= A + by Th49; hence A c= A + by FLANG_1:25; ::_thesis: verum end; theorem Th60: :: FLANG_3:60 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 * ) A1: A * c= (A +) * by Th59, FLANG_1:61; now__::_thesis:_for_x_being_set_st_x_in_(A_*)_+_holds_ x_in_A_* let x be set ; ::_thesis: ( x in (A *) + implies x in A * ) assume x in (A *) + ; ::_thesis: x in A * then consider k being Nat such that 0 < k and A2: x in (A *) |^ k by Th48; (A *) |^ k c= A * by FLANG_1:65; hence x in A * by A2; ::_thesis: verum end; then A3: (A *) + c= A * by TARSKI:def_3; now__::_thesis:_for_x_being_set_st_x_in_(A_+)_*_holds_ x_in_A_* let x be set ; ::_thesis: ( x in (A +) * implies x in A * ) assume x in (A +) * ; ::_thesis: x in A * then consider k being Nat such that A4: x in (A +) |^ k by FLANG_1:41; (A +) |^ k c= A * by Th55, FLANG_1:59; hence x in A * by A4; ::_thesis: verum end; then A5: (A +) * c= A * by TARSKI:def_3; A * c= (A *) + by Th59; hence ( (A *) + = A * & (A +) * = A * ) by A1, A3, A5, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th61: :: FLANG_3:61 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 + c= (B *) + by Th58; hence A + c= B * by Th60; ::_thesis: verum end; theorem :: FLANG_3:62 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 + now__::_thesis:_for_x_being_set_st_x_in_(A_+)_+_holds_ x_in_A_+ let x be set ; ::_thesis: ( x in (A +) + implies b1 in A + ) assume A1: x in (A +) + ; ::_thesis: b1 in A + percases ( x = <%> E or x <> <%> E ) ; suppose x = <%> E ; ::_thesis: b1 in A + hence x in A + by A1, Th56; ::_thesis: verum end; supposeA2: x <> <%> E ; ::_thesis: b1 in A + (A +) + c= A * by Th55, Th61; then x in A * by A1; then A3: x in (A +) \/ {(<%> E)} by Th53; not x in {(<%> E)} by A2, TARSKI:def_1; hence x in A + by A3, XBOOLE_0:def_3; ::_thesis: verum end; end; end; then A4: (A +) + c= A + by TARSKI:def_3; A + c= (A +) + by Th59; hence (A +) + = A + by A4, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: FLANG_3:63 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 + = A |^.. 1 by Th50; hence A + <> {(<%> E)} by A1, A2, Th14; ::_thesis: verum end; theorem :: FLANG_3:64 for E being set for A being Subset of (E ^omega) holds ( A + = {(<%> E)} iff A = {(<%> E)} ) proof let E be set ; ::_thesis: for A being Subset of (E ^omega) holds ( A + = {(<%> E)} iff A = {(<%> E)} ) let A be Subset of (E ^omega); ::_thesis: ( A + = {(<%> E)} iff A = {(<%> E)} ) A + = A |^.. 1 by Th50; hence ( A + = {(<%> E)} iff A = {(<%> E)} ) by Th15; ::_thesis: verum end; theorem :: FLANG_3:65 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 FLANG_2:76 .= A * by Th53 ; ::_thesis: (A ?) + = A * <%> E in A ? by FLANG_2:78; then (A ?) + = (A ?) * by Th57; hence (A ?) + = A * by FLANG_2:85; ::_thesis: verum 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 + proof let E be set ; ::_thesis: 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 + let C be Subset of (E ^omega); ::_thesis: for a, b being Element of E ^omega st a in C + & b in C + holds a ^ b in C + let a, b be Element of E ^omega ; ::_thesis: ( a in C + & b in C + implies a ^ b in C + ) assume that A1: a in C + and A2: b in C + ; ::_thesis: a ^ b in C + consider l being Nat such that l > 0 and A3: b in C |^ l by A2, Th48; consider k being Nat such that A4: k > 0 and A5: a in C |^ k by A1, Th48; a ^ b in C |^ (k + l) by A5, A3, FLANG_1:40; hence a ^ b in C + by A4, Th48; ::_thesis: verum end; theorem :: FLANG_3:67 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 + 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 + let A, C, B be Subset of (E ^omega); ::_thesis: ( A c= C + & B c= C + implies A ^^ B c= C + ) assume that A1: A c= C + and A2: B c= C + ; ::_thesis: A ^^ B c= C + now__::_thesis:_for_x_being_set_st_x_in_A_^^_B_holds_ x_in_C_+ let x be set ; ::_thesis: ( x in A ^^ B implies x in C + ) assume x in A ^^ B ; ::_thesis: x in C + 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 x in C + by A1, A2, Th66; ::_thesis: verum end; hence A ^^ B c= C + by TARSKI:def_3; ::_thesis: verum end; theorem :: FLANG_3:68 for E being set for A being Subset of (E ^omega) holds A ^^ A c= A + proof let E be set ; ::_thesis: for A being Subset of (E ^omega) holds A ^^ A c= A + let A be Subset of (E ^omega); ::_thesis: A ^^ A c= A + A ^^ A = A |^ 2 by FLANG_1:26; hence A ^^ A c= A + by Th49; ::_thesis: verum end; theorem :: FLANG_3:69 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 ) assume that A1: A + = {x} and A2: x <> <%> E ; ::_thesis: contradiction A |^.. 1 = {x} by A1, Th50; hence contradiction by A2, Th38; ::_thesis: verum end; theorem :: FLANG_3:70 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 ^^ (A |^.. 1) by Th50 .= (A |^.. 1) ^^ A by Th23 .= (A +) ^^ A by Th50 ; ::_thesis: verum 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) proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for k being Nat holds (A |^ k) ^^ (A +) = (A +) ^^ (A |^ k) let A be Subset of (E ^omega); ::_thesis: for k being Nat holds (A |^ k) ^^ (A +) = (A +) ^^ (A |^ k) let k be Nat; ::_thesis: (A |^ k) ^^ (A +) = (A +) ^^ (A |^ k) thus (A |^ k) ^^ (A +) = (A |^ k) ^^ (A |^.. 1) by Th50 .= (A |^.. 1) ^^ (A |^ k) by Th24 .= (A +) ^^ (A |^ k) by Th50 ; ::_thesis: verum 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)) 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 Th50 .= (A |^.. 1) ^^ (A |^ (m,n)) by Th25 .= (A +) ^^ (A |^ (m,n)) by Th50 ; ::_thesis: verum end; theorem :: FLANG_3:73 for E being set for B, A being Subset of (E ^omega) st <%> E in B holds ( A c= A ^^ (B +) & A c= (B +) ^^ A ) proof let E be set ; ::_thesis: for B, A being Subset of (E ^omega) st <%> E in B holds ( A c= A ^^ (B +) & A c= (B +) ^^ A ) let B, A be Subset of (E ^omega); ::_thesis: ( <%> E in B implies ( A c= A ^^ (B +) & A c= (B +) ^^ A ) ) assume <%> E in B ; ::_thesis: ( A c= A ^^ (B +) & A c= (B +) ^^ A ) then B + = B * by Th57; hence ( A c= A ^^ (B +) & A c= (B +) ^^ A ) by FLANG_2:18; ::_thesis: verum end; theorem :: FLANG_3:74 for E being set for A being Subset of (E ^omega) holds (A +) ^^ (A +) = A |^.. 2 proof let E be set ; ::_thesis: for A being Subset of (E ^omega) holds (A +) ^^ (A +) = A |^.. 2 let A be Subset of (E ^omega); ::_thesis: (A +) ^^ (A +) = A |^.. 2 thus (A +) ^^ (A +) = (A |^.. 1) ^^ (A +) by Th50 .= (A |^.. 1) ^^ (A |^.. 1) by Th50 .= A |^.. (1 + 1) by Th18 .= A |^.. 2 ; ::_thesis: verum 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) proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for k being Nat holds (A +) ^^ (A |^ k) = A |^.. (k + 1) let A be Subset of (E ^omega); ::_thesis: for k being Nat holds (A +) ^^ (A |^ k) = A |^.. (k + 1) let k be Nat; ::_thesis: (A +) ^^ (A |^ k) = A |^.. (k + 1) thus (A +) ^^ (A |^ k) = (A |^.. 1) ^^ (A |^ k) by Th50 .= A |^.. (k + 1) by Th22 ; ::_thesis: verum end; theorem :: FLANG_3:76 for E being set for A being Subset of (E ^omega) holds (A +) ^^ A = A |^.. 2 proof let E be set ; ::_thesis: for A being Subset of (E ^omega) holds (A +) ^^ A = A |^.. 2 let A be Subset of (E ^omega); ::_thesis: (A +) ^^ A = A |^.. 2 (A +) ^^ A = (A +) ^^ (A |^ 1) by FLANG_1:25 .= A |^.. (1 + 1) by Th75 ; hence (A +) ^^ A = A |^.. 2 ; ::_thesis: verum 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) proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for k, l being Nat st k <= l holds (A +) ^^ (A |^ (k,l)) = A |^.. (k + 1) let A be Subset of (E ^omega); ::_thesis: for k, l being Nat st k <= l holds (A +) ^^ (A |^ (k,l)) = A |^.. (k + 1) let k, l be Nat; ::_thesis: ( k <= l implies (A +) ^^ (A |^ (k,l)) = A |^.. (k + 1) ) assume k <= l ; ::_thesis: (A +) ^^ (A |^ (k,l)) = A |^.. (k + 1) then (A |^.. 1) ^^ (A |^ (k,l)) = A |^.. (1 + k) by Th33; hence (A +) ^^ (A |^ (k,l)) = A |^.. (k + 1) by Th50; ::_thesis: verum 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 + proof let E be set ; ::_thesis: for A, B being Subset of (E ^omega) for n being Nat st A c= B + & n > 0 holds A |^ n c= B + let A, B be Subset of (E ^omega); ::_thesis: for n being Nat st A c= B + & n > 0 holds A |^ n c= B + let n be Nat; ::_thesis: ( A c= B + & n > 0 implies A |^ n c= B + ) assume that A1: A c= B + and A2: n > 0 ; ::_thesis: A |^ n c= B + A c= B |^.. 1 by A1, Th50; then A |^ n c= B |^.. 1 by A2, Th28; hence A |^ n c= B + by Th50; ::_thesis: verum end; theorem :: FLANG_3:79 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 +) ^^ (A |^ (0,1)) by FLANG_2:79 .= (A |^ (0,1)) ^^ (A +) by Th72 .= (A ?) ^^ (A +) by FLANG_2:79 ; ::_thesis: verum end; theorem :: FLANG_3:80 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 ?) = (A |^.. 1) ^^ (A ?) by Th50 .= A |^.. 1 by Th41 .= A + by Th50 ; ::_thesis: verum end; theorem :: FLANG_3:81 for E being set for A being Subset of (E ^omega) holds ( A ? c= A + iff <%> E in A ) proof let E be set ; ::_thesis: for A being Subset of (E ^omega) holds ( A ? c= A + iff <%> E in A ) let A be Subset of (E ^omega); ::_thesis: ( A ? c= A + iff <%> E in A ) A + = A |^.. 1 by Th50; hence ( A ? c= A + iff <%> E in A ) by Th40; ::_thesis: verum end; theorem :: FLANG_3: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 c= B |^.. 1 by Th50; then A |^.. 1 c= B |^.. 1 by Th29; then A + c= B |^.. 1 by Th50; hence A + c= B + by Th50; ::_thesis: verum end; theorem :: FLANG_3:83 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 A c= B + ; ::_thesis: B + = (B \/ A) + then A c= B |^.. 1 by Th50; then B |^.. 1 = (B \/ A) |^.. 1 by Th47; then B |^.. 1 = (B \/ A) + by Th50; hence B + = (B \/ A) + by Th50; ::_thesis: verum end; theorem :: FLANG_3:84 for E being set for A being Subset of (E ^omega) for n being Nat st n > 0 holds A |^.. n c= A + proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for n being Nat st n > 0 holds A |^.. n c= A + let A be Subset of (E ^omega); ::_thesis: for n being Nat st n > 0 holds A |^.. n c= A + let n be Nat; ::_thesis: ( n > 0 implies A |^.. n c= A + ) assume A1: n > 0 ; ::_thesis: A |^.. n c= A + let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A |^.. n or x in A + ) assume x in A |^.. n ; ::_thesis: x in A + then ex k being Nat st ( k >= n & x in A |^ k ) by Th2; hence x in A + by A1, Th48; ::_thesis: verum 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 + proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for m, n being Nat st m > 0 holds A |^ (m,n) c= A + let A be Subset of (E ^omega); ::_thesis: for m, n being Nat st m > 0 holds A |^ (m,n) c= A + let m, n be Nat; ::_thesis: ( m > 0 implies A |^ (m,n) c= A + ) assume A1: m > 0 ; ::_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 FLANG_2:19; hence x in A + by A1, Th48; ::_thesis: verum end; theorem Th86: :: FLANG_3:86 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 *) ^^ (A |^.. 1) by Th50 .= (A |^.. 1) ^^ (A *) by Th32 .= (A +) ^^ (A *) by Th50 ; ::_thesis: verum end; theorem Th87: :: FLANG_3:87 for E being set for A being Subset of (E ^omega) for k being Nat holds (A +) |^ k c= A |^.. k proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for k being Nat holds (A +) |^ k c= A |^.. k let A be Subset of (E ^omega); ::_thesis: for k being Nat holds (A +) |^ k c= A |^.. k let k be Nat; ::_thesis: (A +) |^ k c= A |^.. k percases ( k > 0 or k = 0 ) ; suppose k > 0 ; ::_thesis: (A +) |^ k c= A |^.. k then (A |^.. 1) |^ k c= A |^.. (1 * k) by Th19; hence (A +) |^ k c= A |^.. k by Th50; ::_thesis: verum end; supposeA1: k = 0 ; ::_thesis: (A +) |^ k c= A |^.. k A |^.. 0 = A * by Th11; then A2: <%> E in A |^.. 0 by FLANG_1:48; (A +) |^ k = {(<%> E)} by A1, FLANG_1:24; hence (A +) |^ k c= A |^.. k by A1, A2, ZFMISC_1:31; ::_thesis: verum end; end; 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 proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for m, n being Nat holds (A +) |^ (m,n) c= A |^.. m let A be Subset of (E ^omega); ::_thesis: for m, n being Nat holds (A +) |^ (m,n) c= A |^.. m let m, n be Nat; ::_thesis: (A +) |^ (m,n) c= A |^.. m let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A +) |^ (m,n) or x in A |^.. m ) assume x in (A +) |^ (m,n) ; ::_thesis: x in A |^.. m then consider k being Nat such that A1: m <= k and k <= n and A2: x in (A +) |^ k by FLANG_2:19; (A +) |^ k c= A |^.. k by Th87; then A3: x in A |^.. k by A2; A |^.. k c= A |^.. m by A1, Th5; hence x in A |^.. m by A3; ::_thesis: verum 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 + proof let E be set ; ::_thesis: for A, B being Subset of (E ^omega) for n being Nat st A c= B + & n > 0 holds A |^.. n c= B + let A, B be Subset of (E ^omega); ::_thesis: for n being Nat st A c= B + & n > 0 holds A |^.. n c= B + let n be Nat; ::_thesis: ( A c= B + & n > 0 implies A |^.. n c= B + ) assume that A1: A c= B + and A2: n > 0 ; ::_thesis: A |^.. n c= B + A c= B |^.. 1 by A1, Th50; then A |^.. n c= B |^.. 1 by A2, Th29; hence A |^.. n c= B + by Th50; ::_thesis: verum 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) proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for k being Nat holds (A +) ^^ (A |^.. k) = A |^.. (k + 1) let A be Subset of (E ^omega); ::_thesis: for k being Nat holds (A +) ^^ (A |^.. k) = A |^.. (k + 1) let k be Nat; ::_thesis: (A +) ^^ (A |^.. k) = A |^.. (k + 1) thus (A +) ^^ (A |^.. k) = (A |^.. 1) ^^ (A |^.. k) by Th50 .= A |^.. (k + 1) by Th18 ; ::_thesis: verum 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 +) 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) = A |^.. (k + 1) by Th90 .= (A |^.. k) ^^ (A |^.. 1) by Th18 .= (A |^.. k) ^^ (A +) by Th50 ; ::_thesis: verum end; theorem Th92: :: FLANG_3:92 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 *) = (A |^.. 1) ^^ (A *) by Th50 .= A |^.. 1 by Th17 .= A + by Th50 ; ::_thesis: verum end; theorem :: FLANG_3:93 for E being set for B, A being Subset of (E ^omega) st B c= A * holds ( (A +) ^^ B c= A + & B ^^ (A +) c= A + ) proof let E be set ; ::_thesis: for B, A being Subset of (E ^omega) st B c= A * holds ( (A +) ^^ B c= A + & B ^^ (A +) c= A + ) let B, A be Subset of (E ^omega); ::_thesis: ( B c= A * implies ( (A +) ^^ B c= A + & B ^^ (A +) c= A + ) ) assume A1: B c= A * ; ::_thesis: ( (A +) ^^ B c= A + & B ^^ (A +) c= A + ) then B ^^ (A +) c= (A *) ^^ (A +) by FLANG_1:17; then A2: B ^^ (A +) c= (A +) ^^ (A *) by Th86; (A +) ^^ B c= (A +) ^^ (A *) by A1, FLANG_1:17; hence ( (A +) ^^ B c= A + & B ^^ (A +) c= A + ) by A2, Th92; ::_thesis: verum end; theorem :: FLANG_3:94 for E being set for A, B being Subset of (E ^omega) holds (A /\ B) + c= (A +) /\ (B +) proof let E be set ; ::_thesis: for A, B being Subset of (E ^omega) holds (A /\ B) + c= (A +) /\ (B +) let A, B be Subset of (E ^omega); ::_thesis: (A /\ B) + c= (A +) /\ (B +) A1: A + = A |^.. 1 by Th50; A2: B + = B |^.. 1 by Th50; (A /\ B) + = (A /\ B) |^.. 1 by Th50; hence (A /\ B) + c= (A +) /\ (B +) by A1, A2, Th44; ::_thesis: verum end; theorem :: FLANG_3:95 for E being set for A, B being Subset of (E ^omega) holds (A +) \/ (B +) c= (A \/ B) + proof let E be set ; ::_thesis: for A, B being Subset of (E ^omega) holds (A +) \/ (B +) c= (A \/ B) + let A, B be Subset of (E ^omega); ::_thesis: (A +) \/ (B +) c= (A \/ B) + A1: A + = A |^.. 1 by Th50; A2: B + = B |^.. 1 by Th50; (A \/ B) + = (A \/ B) |^.. 1 by Th50; hence (A +) \/ (B +) c= (A \/ B) + by A1, A2, Th45; ::_thesis: verum end; theorem :: FLANG_3:96 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 |^.. 1 by Th50; hence ( <%x%> in A + iff <%x%> in A ) by Th46; ::_thesis: verum end;