:: FLANG_1 semantic presentation begin definition let E be set ; let a, b be Element of E ^omega ; :: original: ^ redefine funca ^ b -> Element of E ^omega ; coherence a ^ b is Element of E ^omega by AFINSQ_1:def_7; end; definition let E be set ; :: original: <%> redefine func <%> E -> Element of E ^omega ; coherence <%> E is Element of E ^omega by AFINSQ_1:def_7; end; definition let E be non empty set ; let e be Element of E; :: original: <% redefine func<%e%> -> Element of E ^omega ; coherence <%e%> is Element of E ^omega by AFINSQ_1:def_7; end; definition let E be set ; let a be Element of E ^omega ; :: original: { redefine func{a} -> Subset of (E ^omega); coherence {a} is Subset of (E ^omega) by SUBSET_1:33; end; definition let E be set ; let f be Function of NAT,(bool E); let n be Nat; :: original: . redefine funcf . n -> Subset of E; coherence f . n is Subset of E proof n is Element of NAT by ORDINAL1:def_12; then f . n in rng f by FUNCT_2:112; hence f . n is Subset of E ; ::_thesis: verum end; end; theorem Th1: :: FLANG_1:1 for n1, n, n2 being Nat st ( n1 > n or n2 > n ) holds n1 + n2 > n proof let n1, n, n2 be Nat; ::_thesis: ( ( n1 > n or n2 > n ) implies n1 + n2 > n ) A1: ( n1 > n & n2 >= 0 implies n1 + n2 > n + 0 ) by XREAL_1:8; A2: ( n1 >= 0 & n2 > n implies n1 + n2 > n + 0 ) by XREAL_1:8; assume ( n1 > n or n2 > n ) ; ::_thesis: n1 + n2 > n hence n1 + n2 > n by A1, A2; ::_thesis: verum end; theorem Th2: :: FLANG_1:2 for n1, n, n2 being Nat st n1 + n <= n2 + 1 & n > 0 holds n1 <= n2 proof let n1, n, n2 be Nat; ::_thesis: ( n1 + n <= n2 + 1 & n > 0 implies n1 <= n2 ) assume that A1: n1 + n <= n2 + 1 and A2: n > 0 ; ::_thesis: n1 <= n2 1 + 0 <= n by A2, NAT_1:13; hence n1 <= n2 by A1, XREAL_1:8; ::_thesis: verum end; theorem Th3: :: FLANG_1:3 for n1, n2 being Nat holds ( n1 + n2 = 1 iff ( ( n1 = 1 & n2 = 0 ) or ( n1 = 0 & n2 = 1 ) ) ) proof let n1, n2 be Nat; ::_thesis: ( n1 + n2 = 1 iff ( ( n1 = 1 & n2 = 0 ) or ( n1 = 0 & n2 = 1 ) ) ) thus ( not n1 + n2 = 1 or ( n1 = 1 & n2 = 0 ) or ( n1 = 0 & n2 = 1 ) ) ::_thesis: ( ( ( n1 = 1 & n2 = 0 ) or ( n1 = 0 & n2 = 1 ) ) implies n1 + n2 = 1 ) proof assume A1: n1 + n2 = 1 ; ::_thesis: ( ( n1 = 1 & n2 = 0 ) or ( n1 = 0 & n2 = 1 ) ) now__::_thesis:_(_n1_<=_1_&_n2_<=_1_&_not_(_n1_=_1_&_n2_=_0_)_implies_(_n1_=_0_&_n2_=_1_)_) A2: ( n1 = 0 implies not n2 = 0 ) by A1; assume A3: ( n1 <= 1 & n2 <= 1 ) ; ::_thesis: ( ( n1 = 1 & n2 = 0 ) or ( n1 = 0 & n2 = 1 ) ) ( n1 = 1 implies not n2 = 1 ) by A1; hence ( ( n1 = 1 & n2 = 0 ) or ( n1 = 0 & n2 = 1 ) ) by A3, A2, NAT_1:25; ::_thesis: verum end; hence ( ( n1 = 1 & n2 = 0 ) or ( n1 = 0 & n2 = 1 ) ) by A1, Th1; ::_thesis: verum end; thus ( ( ( n1 = 1 & n2 = 0 ) or ( n1 = 0 & n2 = 1 ) ) implies n1 + n2 = 1 ) ; ::_thesis: verum end; theorem Th4: :: FLANG_1:4 for x, E being set for a, b being Element of E ^omega holds ( a ^ b = <%x%> iff ( ( a = <%> E & b = <%x%> ) or ( b = <%> E & a = <%x%> ) ) ) proof let x, E be set ; ::_thesis: for a, b being Element of E ^omega holds ( a ^ b = <%x%> iff ( ( a = <%> E & b = <%x%> ) or ( b = <%> E & a = <%x%> ) ) ) let a, b be Element of E ^omega ; ::_thesis: ( a ^ b = <%x%> iff ( ( a = <%> E & b = <%x%> ) or ( b = <%> E & a = <%x%> ) ) ) A1: ( {} ^ b = b & a ^ {} = a ) ; thus ( not a ^ b = <%x%> or ( a = <%> E & b = <%x%> ) or ( b = <%> E & a = <%x%> ) ) ::_thesis: ( ( ( a = <%> E & b = <%x%> ) or ( b = <%> E & a = <%x%> ) ) implies a ^ b = <%x%> ) proof assume A2: a ^ b = <%x%> ; ::_thesis: ( ( a = <%> E & b = <%x%> ) or ( b = <%> E & a = <%x%> ) ) then len (a ^ b) = 1 by AFINSQ_1:34; then (len a) + (len b) = 1 by AFINSQ_1:17; then ( ( len a = 1 & b = <%> E ) or ( a = <%> E & len b = 1 ) ) by Th3; hence ( ( a = <%> E & b = <%x%> ) or ( b = <%> E & a = <%x%> ) ) by A2, A1; ::_thesis: verum end; assume ( ( a = <%> E & b = <%x%> ) or ( b = <%> E & a = <%x%> ) ) ; ::_thesis: a ^ b = <%x%> hence a ^ b = <%x%> by A1; ::_thesis: verum end; theorem Th5: :: FLANG_1:5 for E being set for a being Element of E ^omega for p, q being XFinSequence st a = p ^ q holds ( p is Element of E ^omega & q is Element of E ^omega ) proof let E be set ; ::_thesis: for a being Element of E ^omega for p, q being XFinSequence st a = p ^ q holds ( p is Element of E ^omega & q is Element of E ^omega ) let a be Element of E ^omega ; ::_thesis: for p, q being XFinSequence st a = p ^ q holds ( p is Element of E ^omega & q is Element of E ^omega ) let p, q be XFinSequence; ::_thesis: ( a = p ^ q implies ( p is Element of E ^omega & q is Element of E ^omega ) ) assume a = p ^ q ; ::_thesis: ( p is Element of E ^omega & q is Element of E ^omega ) then ( p is XFinSequence of & q is XFinSequence of ) by AFINSQ_1:31; hence ( p is Element of E ^omega & q is Element of E ^omega ) by AFINSQ_1:def_7; ::_thesis: verum end; theorem Th6: :: FLANG_1:6 for x, E being set st <%x%> is Element of E ^omega holds x in E proof let x, E be set ; ::_thesis: ( <%x%> is Element of E ^omega implies x in E ) assume <%x%> is Element of E ^omega ; ::_thesis: x in E then rng <%x%> c= E by RELAT_1:def_19; then {x} c= E by AFINSQ_1:33; hence x in E by ZFMISC_1:31; ::_thesis: verum end; theorem Th7: :: FLANG_1:7 for E being set for b being Element of E ^omega for n being Nat st len b = n + 1 holds ex c being Element of E ^omega ex e being Element of E st ( len c = n & b = c ^ <%e%> ) proof let E be set ; ::_thesis: for b being Element of E ^omega for n being Nat st len b = n + 1 holds ex c being Element of E ^omega ex e being Element of E st ( len c = n & b = c ^ <%e%> ) let b be Element of E ^omega ; ::_thesis: for n being Nat st len b = n + 1 holds ex c being Element of E ^omega ex e being Element of E st ( len c = n & b = c ^ <%e%> ) let n be Nat; ::_thesis: ( len b = n + 1 implies ex c being Element of E ^omega ex e being Element of E st ( len c = n & b = c ^ <%e%> ) ) assume A1: len b = n + 1 ; ::_thesis: ex c being Element of E ^omega ex e being Element of E st ( len c = n & b = c ^ <%e%> ) then b <> {} ; then consider c9 being XFinSequence, x being set such that A2: b = c9 ^ <%x%> by AFINSQ_1:40; <%x%> is Element of E ^omega by A2, Th5; then reconsider e = x as Element of E by Th6; reconsider c = c9 as Element of E ^omega by A2, Th5; take c ; ::_thesis: ex e being Element of E st ( len c = n & b = c ^ <%e%> ) take e ; ::_thesis: ( len c = n & b = c ^ <%e%> ) n + 1 = (len c) + (len <%x%>) by A1, A2, AFINSQ_1:17 .= (len c) + 1 by AFINSQ_1:33 ; hence ( len c = n & b = c ^ <%e%> ) by A2; ::_thesis: verum end; theorem Th8: :: FLANG_1:8 for p being XFinSequence st p <> {} holds ex q being XFinSequence ex x being set st p = <%x%> ^ q proof let p be XFinSequence; ::_thesis: ( p <> {} implies ex q being XFinSequence ex x being set st p = <%x%> ^ q ) defpred S1[ Nat] means for p being XFinSequence st len p = $1 & p <> {} holds ex q being XFinSequence ex x being set st p = <%x%> ^ q; 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] thus S1[n + 1] ::_thesis: verum proof let p be XFinSequence; ::_thesis: ( len p = n + 1 & p <> {} implies ex q being XFinSequence ex x being set st p = <%x%> ^ q ) assume that A3: len p = n + 1 and A4: p <> {} ; ::_thesis: ex q being XFinSequence ex x being set st p = <%x%> ^ q consider q being XFinSequence, x being set such that A5: p = q ^ <%x%> by A4, AFINSQ_1:40; A6: n + 1 = (len q) + (len <%x%>) by A3, A5, AFINSQ_1:17 .= (len q) + 1 by AFINSQ_1:33 ; percases ( q = {} or q <> {} ) ; suppose q = {} ; ::_thesis: ex q being XFinSequence ex x being set st p = <%x%> ^ q then p = {} ^ <%x%> by A5 .= <%x%> ^ {} ; hence ex q being XFinSequence ex x being set st p = <%x%> ^ q ; ::_thesis: verum end; suppose q <> {} ; ::_thesis: ex q being XFinSequence ex x being set st p = <%x%> ^ q then consider r being XFinSequence, y being set such that A7: q = <%y%> ^ r by A2, A6; p = <%y%> ^ (r ^ <%x%>) by A5, A7, AFINSQ_1:27; hence ex q being XFinSequence ex x being set st p = <%x%> ^ q ; ::_thesis: verum end; end; end; end; A8: S1[ 0 ] ; A9: for n being Nat holds S1[n] from NAT_1:sch_2(A8, A1); A10: len p = len p ; assume p <> {} ; ::_thesis: ex q being XFinSequence ex x being set st p = <%x%> ^ q hence ex q being XFinSequence ex x being set st p = <%x%> ^ q by A9, A10; ::_thesis: verum end; theorem :: FLANG_1:9 for E being set for b being Element of E ^omega for n being Nat st len b = n + 1 holds ex c being Element of E ^omega ex e being Element of E st ( len c = n & b = <%e%> ^ c ) proof let E be set ; ::_thesis: for b being Element of E ^omega for n being Nat st len b = n + 1 holds ex c being Element of E ^omega ex e being Element of E st ( len c = n & b = <%e%> ^ c ) let b be Element of E ^omega ; ::_thesis: for n being Nat st len b = n + 1 holds ex c being Element of E ^omega ex e being Element of E st ( len c = n & b = <%e%> ^ c ) let n be Nat; ::_thesis: ( len b = n + 1 implies ex c being Element of E ^omega ex e being Element of E st ( len c = n & b = <%e%> ^ c ) ) assume A1: len b = n + 1 ; ::_thesis: ex c being Element of E ^omega ex e being Element of E st ( len c = n & b = <%e%> ^ c ) then b <> {} ; then consider c9 being XFinSequence, x being set such that A2: b = <%x%> ^ c9 by Th8; <%x%> is Element of E ^omega by A2, Th5; then reconsider e = x as Element of E by Th6; reconsider c = c9 as Element of E ^omega by A2, Th5; take c ; ::_thesis: ex e being Element of E st ( len c = n & b = <%e%> ^ c ) take e ; ::_thesis: ( len c = n & b = <%e%> ^ c ) n + 1 = (len c) + (len <%x%>) by A1, A2, AFINSQ_1:17 .= (len c) + 1 by AFINSQ_1:33 ; hence ( len c = n & b = <%e%> ^ c ) by A2; ::_thesis: verum end; Lm1: for i, j being Nat for p being XFinSequence st len p = i + j holds ex q1, q2 being XFinSequence st ( len q1 = i & len q2 = j & p = q1 ^ q2 ) by AFINSQ_1:61; theorem :: FLANG_1:10 for E being set for b being Element of E ^omega for n, m being Nat st len b = n + m holds ex c1, c2 being Element of E ^omega st ( len c1 = n & len c2 = m & b = c1 ^ c2 ) proof let E be set ; ::_thesis: for b being Element of E ^omega for n, m being Nat st len b = n + m holds ex c1, c2 being Element of E ^omega st ( len c1 = n & len c2 = m & b = c1 ^ c2 ) let b be Element of E ^omega ; ::_thesis: for n, m being Nat st len b = n + m holds ex c1, c2 being Element of E ^omega st ( len c1 = n & len c2 = m & b = c1 ^ c2 ) let n, m be Nat; ::_thesis: ( len b = n + m implies ex c1, c2 being Element of E ^omega st ( len c1 = n & len c2 = m & b = c1 ^ c2 ) ) assume len b = n + m ; ::_thesis: ex c1, c2 being Element of E ^omega st ( len c1 = n & len c2 = m & b = c1 ^ c2 ) then consider c19, c29 being XFinSequence such that A1: ( len c19 = n & len c29 = m ) and A2: b = c19 ^ c29 by Lm1; reconsider c2 = c29 as Element of E ^omega by A2, Th5; reconsider c1 = c19 as Element of E ^omega by A2, Th5; take c1 ; ::_thesis: ex c2 being Element of E ^omega st ( len c1 = n & len c2 = m & b = c1 ^ c2 ) take c2 ; ::_thesis: ( len c1 = n & len c2 = m & b = c1 ^ c2 ) thus ( len c1 = n & len c2 = m & b = c1 ^ c2 ) by A1, A2; ::_thesis: verum end; theorem Th11: :: FLANG_1:11 for E being set for a being Element of E ^omega st a ^ a = a holds a = {} proof let E be set ; ::_thesis: for a being Element of E ^omega st a ^ a = a holds a = {} let a be Element of E ^omega ; ::_thesis: ( a ^ a = a implies a = {} ) assume a ^ a = a ; ::_thesis: a = {} then (len a) + (len a) = len a by AFINSQ_1:17; hence a = {} ; ::_thesis: verum end; begin definition let E be set ; let A, B be Subset of (E ^omega); funcA ^^ B -> Subset of (E ^omega) means :Def1: :: FLANG_1:def 1 for x being set holds ( x in it iff ex a, b being Element of E ^omega st ( a in A & b in B & x = a ^ b ) ); existence ex b1 being Subset of (E ^omega) st for x being set holds ( x in b1 iff ex a, b being Element of E ^omega st ( a in A & b in B & x = a ^ b ) ) proof defpred S1[ set ] means ex a, b being Element of E ^omega st ( a in A & b in B & $1 = a ^ b ); consider C being Subset of (E ^omega) such that A1: for x being set holds ( x in C iff ( x in E ^omega & S1[x] ) ) from SUBSET_1:sch_1(); take C ; ::_thesis: for x being set holds ( x in C iff ex a, b being Element of E ^omega st ( a in A & b in B & x = a ^ b ) ) thus for x being set holds ( x in C iff ex a, b being Element of E ^omega st ( a in A & b in B & x = a ^ b ) ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Subset of (E ^omega) st ( for x being set holds ( x in b1 iff ex a, b being Element of E ^omega st ( a in A & b in B & x = a ^ b ) ) ) & ( for x being set holds ( x in b2 iff ex a, b being Element of E ^omega st ( a in A & b in B & x = a ^ b ) ) ) holds b1 = b2 proof let C1, C2 be Subset of (E ^omega); ::_thesis: ( ( for x being set holds ( x in C1 iff ex a, b being Element of E ^omega st ( a in A & b in B & x = a ^ b ) ) ) & ( for x being set holds ( x in C2 iff ex a, b being Element of E ^omega st ( a in A & b in B & x = a ^ b ) ) ) implies C1 = C2 ) assume that A2: for x being set holds ( x in C1 iff ex a, b being Element of E ^omega st ( a in A & b in B & x = a ^ b ) ) and A3: for x being set holds ( x in C2 iff ex a, b being Element of E ^omega st ( a in A & b in B & x = a ^ b ) ) ; ::_thesis: C1 = C2 now__::_thesis:_for_x_being_set_holds_ (_(_x_in_C1_implies_x_in_C2_)_&_(_x_in_C2_implies_x_in_C1_)_) let x be set ; ::_thesis: ( ( x in C1 implies x in C2 ) & ( x in C2 implies x in C1 ) ) thus ( x in C1 implies x in C2 ) ::_thesis: ( x in C2 implies x in C1 ) proof assume x in C1 ; ::_thesis: x in C2 then ex a, b being Element of E ^omega st ( a in A & b in B & x = a ^ b ) by A2; hence x in C2 by A3; ::_thesis: verum end; assume x in C2 ; ::_thesis: x in C1 then ex a, b being Element of E ^omega st ( a in A & b in B & x = a ^ b ) by A3; hence x in C1 by A2; ::_thesis: verum end; hence C1 = C2 by TARSKI:1; ::_thesis: verum end; end; :: deftheorem Def1 defines ^^ FLANG_1:def_1_:_ for E being set for A, B, b4 being Subset of (E ^omega) holds ( b4 = A ^^ B iff for x being set holds ( x in b4 iff ex a, b being Element of E ^omega st ( a in A & b in B & x = a ^ b ) ) ); theorem Th12: :: FLANG_1:12 for E being set for A, B being Subset of (E ^omega) holds ( A ^^ B = {} iff ( A = {} or B = {} ) ) proof let E be set ; ::_thesis: for A, B being Subset of (E ^omega) holds ( A ^^ B = {} iff ( A = {} or B = {} ) ) let A, B be Subset of (E ^omega); ::_thesis: ( A ^^ B = {} iff ( A = {} or B = {} ) ) thus ( not A ^^ B = {} or A = {} or B = {} ) ::_thesis: ( ( A = {} or B = {} ) implies A ^^ B = {} ) proof assume that A1: A ^^ B = {} and A2: A <> {} and A3: B <> {} ; ::_thesis: contradiction consider a being Element of E ^omega such that A4: a in A by A2, SUBSET_1:4; consider b being Element of E ^omega such that A5: b in B by A3, SUBSET_1:4; a ^ b in A ^^ B by A4, A5, Def1; hence contradiction by A1; ::_thesis: verum end; assume A6: ( A = {} or B = {} ) ; ::_thesis: A ^^ B = {} for x being set holds not x in A ^^ B proof given x being set such that A7: x in A ^^ B ; ::_thesis: contradiction ex a, b being Element of E ^omega st ( a in A & b in B & x = a ^ b ) by A7, Def1; hence contradiction by A6; ::_thesis: verum end; hence A ^^ B = {} by XBOOLE_0:def_1; ::_thesis: verum end; theorem Th13: :: FLANG_1:13 for E being set for A being Subset of (E ^omega) holds ( A ^^ {(<%> E)} = A & {(<%> E)} ^^ A = A ) proof let E be set ; ::_thesis: for A being Subset of (E ^omega) holds ( A ^^ {(<%> E)} = A & {(<%> E)} ^^ A = A ) let A be Subset of (E ^omega); ::_thesis: ( A ^^ {(<%> E)} = A & {(<%> E)} ^^ A = A ) A1: for x being set st x in A ^^ {(<%> E)} holds x in A proof let x be set ; ::_thesis: ( x in A ^^ {(<%> E)} implies x in A ) assume x in A ^^ {(<%> E)} ; ::_thesis: x in A then consider a, d being Element of E ^omega such that A2: a in A and A3: ( d in {(<%> E)} & x = a ^ d ) by Def1; x = a ^ {} by A3, TARSKI:def_1; hence x in A by A2; ::_thesis: verum end; A4: for x being set st x in A holds x in {(<%> E)} ^^ A proof let x be set ; ::_thesis: ( x in A implies x in {(<%> E)} ^^ A ) assume A5: x in A ; ::_thesis: x in {(<%> E)} ^^ A ex d, a being Element of E ^omega st ( d in {(<%> E)} & a in A & x = d ^ a ) proof reconsider a = x as Element of E ^omega by A5; consider d being Element of E ^omega such that A6: d = <%> E ; take d ; ::_thesis: ex a being Element of E ^omega st ( d in {(<%> E)} & a in A & x = d ^ a ) take a ; ::_thesis: ( d in {(<%> E)} & a in A & x = d ^ a ) {} ^ a = a ; hence ( d in {(<%> E)} & a in A & x = d ^ a ) by A5, A6, TARSKI:def_1; ::_thesis: verum end; hence x in {(<%> E)} ^^ A by Def1; ::_thesis: verum end; A7: for x being set st x in A holds x in A ^^ {(<%> E)} proof let x be set ; ::_thesis: ( x in A implies x in A ^^ {(<%> E)} ) assume A8: x in A ; ::_thesis: x in A ^^ {(<%> E)} ex a, d being Element of E ^omega st ( a in A & d in {(<%> E)} & x = a ^ d ) proof reconsider a = x as Element of E ^omega by A8; set d = <%> E; take a ; ::_thesis: ex d being Element of E ^omega st ( a in A & d in {(<%> E)} & x = a ^ d ) take <%> E ; ::_thesis: ( a in A & <%> E in {(<%> E)} & x = a ^ (<%> E) ) a ^ {} = a ; hence ( a in A & <%> E in {(<%> E)} & x = a ^ (<%> E) ) by A8, TARSKI:def_1; ::_thesis: verum end; hence x in A ^^ {(<%> E)} by Def1; ::_thesis: verum end; for x being set st x in {(<%> E)} ^^ A holds x in A proof let x be set ; ::_thesis: ( x in {(<%> E)} ^^ A implies x in A ) assume x in {(<%> E)} ^^ A ; ::_thesis: x in A then consider d, a being Element of E ^omega such that A9: d in {(<%> E)} and A10: a in A and A11: x = d ^ a by Def1; x = {} ^ a by A9, A11, TARSKI:def_1; hence x in A by A10; ::_thesis: verum end; hence ( A ^^ {(<%> E)} = A & {(<%> E)} ^^ A = A ) by A1, A4, A7, TARSKI:1; ::_thesis: verum end; theorem Th14: :: FLANG_1:14 for E being set for A, B being Subset of (E ^omega) holds ( A ^^ B = {(<%> E)} iff ( A = {(<%> E)} & B = {(<%> E)} ) ) proof let E be set ; ::_thesis: for A, B being Subset of (E ^omega) holds ( A ^^ B = {(<%> E)} iff ( A = {(<%> E)} & B = {(<%> E)} ) ) let A, B be Subset of (E ^omega); ::_thesis: ( A ^^ B = {(<%> E)} iff ( A = {(<%> E)} & B = {(<%> E)} ) ) thus ( A ^^ B = {(<%> E)} implies ( A = {(<%> E)} & B = {(<%> E)} ) ) ::_thesis: ( A = {(<%> E)} & B = {(<%> E)} implies A ^^ B = {(<%> E)} ) proof assume that A1: A ^^ B = {(<%> E)} and A2: ( A <> {(<%> E)} or B <> {(<%> E)} ) ; ::_thesis: contradiction <%> E in A ^^ B by A1, TARSKI:def_1; then consider a, b being Element of E ^omega such that A3: a in A and A4: b in B and <%> E = a ^ b by Def1; A5: now__::_thesis:_for_x_being_set_st_(_x_in_A_or_x_in_B_)_holds_ not_x_<>_<%>_E let x be set ; ::_thesis: ( ( x in A or x in B ) implies not x <> <%> E ) assume that A6: ( x in A or x in B ) and A7: x <> <%> E ; ::_thesis: contradiction A8: now__::_thesis:_not_x_in_B assume A9: x in B ; ::_thesis: contradiction then reconsider xb = x as Element of E ^omega ; A10: a ^ xb <> <%> E by A7, AFINSQ_1:30; a ^ xb in A ^^ B by A3, A9, Def1; hence contradiction by A1, A10, TARSKI:def_1; ::_thesis: verum end; now__::_thesis:_not_x_in_A assume A11: x in A ; ::_thesis: contradiction then reconsider xa = x as Element of E ^omega ; A12: xa ^ b <> <%> E by A7, AFINSQ_1:30; xa ^ b in A ^^ B by A4, A11, Def1; hence contradiction by A1, A12, TARSKI:def_1; ::_thesis: verum end; hence contradiction by A6, A8; ::_thesis: verum end; then A13: for x being set holds ( x in B iff x = <%> E ) by A4; for x being set holds ( x in A iff x = <%> E ) by A3, A5; hence contradiction by A2, A13, TARSKI:def_1; ::_thesis: verum end; assume ( A = {(<%> E)} & B = {(<%> E)} ) ; ::_thesis: A ^^ B = {(<%> E)} hence A ^^ B = {(<%> E)} by Th13; ::_thesis: verum end; theorem Th15: :: FLANG_1:15 for E being set for A, B being Subset of (E ^omega) holds ( <%> E in A ^^ B iff ( <%> E in A & <%> E in B ) ) proof let E be set ; ::_thesis: for A, B being Subset of (E ^omega) holds ( <%> E in A ^^ B iff ( <%> E in A & <%> E in B ) ) let A, B be Subset of (E ^omega); ::_thesis: ( <%> E in A ^^ B iff ( <%> E in A & <%> E in B ) ) thus ( <%> E in A ^^ B implies ( <%> E in A & <%> E in B ) ) ::_thesis: ( <%> E in A & <%> E in B implies <%> E in A ^^ B ) proof assume <%> E in A ^^ B ; ::_thesis: ( <%> E in A & <%> E in B ) then ex a, b being Element of E ^omega st ( a in A & b in B & a ^ b = <%> E ) by Def1; hence ( <%> E in A & <%> E in B ) by AFINSQ_1:30; ::_thesis: verum end; assume ( <%> E in A & <%> E in B ) ; ::_thesis: <%> E in A ^^ B then {} ^ (<%> E) in A ^^ B by Def1; hence <%> E in A ^^ B ; ::_thesis: verum end; theorem Th16: :: FLANG_1:16 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 A1: <%> E in B ; ::_thesis: ( A c= A ^^ B & A c= B ^^ A ) thus A c= A ^^ B ::_thesis: A c= B ^^ A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in A ^^ B ) assume A2: x in A ; ::_thesis: x in A ^^ B then reconsider xa = x as Element of E ^omega ; xa ^ {} in A ^^ B by A1, A2, Def1; hence x in A ^^ B ; ::_thesis: verum end; thus A c= B ^^ A ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in B ^^ A ) assume A3: x in A ; ::_thesis: x in B ^^ A then reconsider xa = x as Element of E ^omega ; {} ^ xa in B ^^ A by A1, A3, Def1; hence x in B ^^ A ; ::_thesis: verum end; end; theorem Th17: :: FLANG_1:17 for E being set for A, C, B, D being Subset of (E ^omega) st A c= C & B c= D holds A ^^ B c= C ^^ D proof let E be set ; ::_thesis: for A, C, B, D being Subset of (E ^omega) st A c= C & B c= D holds A ^^ B c= C ^^ D let A, C, B, D be Subset of (E ^omega); ::_thesis: ( A c= C & B c= D implies A ^^ B c= C ^^ D ) assume A1: ( A c= C & B c= D ) ; ::_thesis: A ^^ B c= C ^^ D thus A ^^ B c= C ^^ D ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A ^^ B or x in C ^^ D ) assume x in A ^^ B ; ::_thesis: x in C ^^ D then ex a, b being Element of E ^omega st ( a in A & b in B & x = a ^ b ) by Def1; hence x in C ^^ D by A1, Def1; ::_thesis: verum end; end; theorem Th18: :: FLANG_1:18 for E being set for A, B, C being Subset of (E ^omega) holds (A ^^ B) ^^ C = A ^^ (B ^^ C) proof let E be set ; ::_thesis: for A, B, C being Subset of (E ^omega) holds (A ^^ B) ^^ C = A ^^ (B ^^ C) let A, B, C be Subset of (E ^omega); ::_thesis: (A ^^ B) ^^ C = A ^^ (B ^^ C) now__::_thesis:_for_x_being_set_holds_ (_(_x_in_(A_^^_B)_^^_C_implies_x_in_A_^^_(B_^^_C)_)_&_(_x_in_A_^^_(B_^^_C)_implies_x_in_(A_^^_B)_^^_C_)_) let x be set ; ::_thesis: ( ( x in (A ^^ B) ^^ C implies x in A ^^ (B ^^ C) ) & ( x in A ^^ (B ^^ C) implies x in (A ^^ B) ^^ C ) ) thus ( x in (A ^^ B) ^^ C implies x in A ^^ (B ^^ C) ) ::_thesis: ( x in A ^^ (B ^^ C) implies x in (A ^^ B) ^^ C ) proof assume x in (A ^^ B) ^^ C ; ::_thesis: x in A ^^ (B ^^ C) then consider ab, c being Element of E ^omega such that A1: ab in A ^^ B and A2: ( c in C & x = ab ^ c ) by Def1; consider a, b being Element of E ^omega such that A3: a in A and A4: ( b in B & ab = a ^ b ) by A1, Def1; ( x = a ^ (b ^ c) & b ^ c in B ^^ C ) by A2, A4, Def1, AFINSQ_1:27; hence x in A ^^ (B ^^ C) by A3, Def1; ::_thesis: verum end; assume x in A ^^ (B ^^ C) ; ::_thesis: x in (A ^^ B) ^^ C then consider a, bc being Element of E ^omega such that A5: a in A and A6: bc in B ^^ C and A7: x = a ^ bc by Def1; consider b, c being Element of E ^omega such that A8: b in B and A9: c in C and A10: bc = b ^ c by A6, Def1; ( x = (a ^ b) ^ c & a ^ b in A ^^ B ) by A5, A7, A8, A10, Def1, AFINSQ_1:27; hence x in (A ^^ B) ^^ C by A9, Def1; ::_thesis: verum end; hence (A ^^ B) ^^ C = A ^^ (B ^^ C) by TARSKI:1; ::_thesis: verum end; theorem Th19: :: FLANG_1:19 for E being set for A, B, C being Subset of (E ^omega) holds ( A ^^ (B /\ C) c= (A ^^ B) /\ (A ^^ C) & (B /\ C) ^^ A c= (B ^^ A) /\ (C ^^ A) ) proof let E be set ; ::_thesis: for A, B, C being Subset of (E ^omega) holds ( A ^^ (B /\ C) c= (A ^^ B) /\ (A ^^ C) & (B /\ C) ^^ A c= (B ^^ A) /\ (C ^^ A) ) let A, B, C be Subset of (E ^omega); ::_thesis: ( A ^^ (B /\ C) c= (A ^^ B) /\ (A ^^ C) & (B /\ C) ^^ A c= (B ^^ A) /\ (C ^^ A) ) thus A ^^ (B /\ C) c= (A ^^ B) /\ (A ^^ C) ::_thesis: (B /\ C) ^^ A c= (B ^^ A) /\ (C ^^ A) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A ^^ (B /\ C) or x in (A ^^ B) /\ (A ^^ C) ) assume x in A ^^ (B /\ C) ; ::_thesis: x in (A ^^ B) /\ (A ^^ C) then consider a, bc being Element of E ^omega such that A1: a in A and A2: bc in B /\ C and A3: x = a ^ bc by Def1; bc in C by A2, XBOOLE_0:def_4; then A4: x in A ^^ C by A1, A3, Def1; bc in B by A2, XBOOLE_0:def_4; then x in A ^^ B by A1, A3, Def1; hence x in (A ^^ B) /\ (A ^^ C) by A4, XBOOLE_0:def_4; ::_thesis: verum end; thus (B /\ C) ^^ A c= (B ^^ A) /\ (C ^^ A) ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (B /\ C) ^^ A or x in (B ^^ A) /\ (C ^^ A) ) assume x in (B /\ C) ^^ A ; ::_thesis: x in (B ^^ A) /\ (C ^^ A) then consider bc, a being Element of E ^omega such that A5: bc in B /\ C and A6: ( a in A & x = bc ^ a ) by Def1; bc in C by A5, XBOOLE_0:def_4; then A7: x in C ^^ A by A6, Def1; bc in B by A5, XBOOLE_0:def_4; then x in B ^^ A by A6, Def1; hence x in (B ^^ A) /\ (C ^^ A) by A7, XBOOLE_0:def_4; ::_thesis: verum end; end; theorem Th20: :: FLANG_1:20 for E being set for A, B, C being Subset of (E ^omega) holds ( (A ^^ B) \/ (A ^^ C) = A ^^ (B \/ C) & (B ^^ A) \/ (C ^^ A) = (B \/ C) ^^ A ) proof let E be set ; ::_thesis: for A, B, C being Subset of (E ^omega) holds ( (A ^^ B) \/ (A ^^ C) = A ^^ (B \/ C) & (B ^^ A) \/ (C ^^ A) = (B \/ C) ^^ A ) let A, B, C be Subset of (E ^omega); ::_thesis: ( (A ^^ B) \/ (A ^^ C) = A ^^ (B \/ C) & (B ^^ A) \/ (C ^^ A) = (B \/ C) ^^ A ) A1: A ^^ (B \/ C) c= (A ^^ B) \/ (A ^^ C) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A ^^ (B \/ C) or x in (A ^^ B) \/ (A ^^ C) ) assume x in A ^^ (B \/ C) ; ::_thesis: x in (A ^^ B) \/ (A ^^ C) then consider a, bc being Element of E ^omega such that A2: a in A and A3: bc in B \/ C and A4: x = a ^ bc by Def1; ( bc in B or bc in C ) by A3, XBOOLE_0:def_3; then ( x in A ^^ B or x in A ^^ C ) by A2, A4, Def1; hence x in (A ^^ B) \/ (A ^^ C) by XBOOLE_0:def_3; ::_thesis: verum end; A5: (B \/ C) ^^ A c= (B ^^ A) \/ (C ^^ A) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (B \/ C) ^^ A or x in (B ^^ A) \/ (C ^^ A) ) assume x in (B \/ C) ^^ A ; ::_thesis: x in (B ^^ A) \/ (C ^^ A) then consider bc, a being Element of E ^omega such that A6: bc in B \/ C and A7: ( a in A & x = bc ^ a ) by Def1; ( bc in B or bc in C ) by A6, XBOOLE_0:def_3; then ( x in B ^^ A or x in C ^^ A ) by A7, Def1; hence x in (B ^^ A) \/ (C ^^ A) by XBOOLE_0:def_3; ::_thesis: verum end; C c= B \/ C by XBOOLE_1:7; then A8: C ^^ A c= (B \/ C) ^^ A by Th17; B c= B \/ C by XBOOLE_1:7; then B ^^ A c= (B \/ C) ^^ A by Th17; then A9: (B ^^ A) \/ (C ^^ A) c= (B \/ C) ^^ A by A8, XBOOLE_1:8; C c= B \/ C by XBOOLE_1:7; then A10: A ^^ C c= A ^^ (B \/ C) by Th17; B c= B \/ C by XBOOLE_1:7; then A ^^ B c= A ^^ (B \/ C) by Th17; then (A ^^ B) \/ (A ^^ C) c= A ^^ (B \/ C) by A10, XBOOLE_1:8; hence ( (A ^^ B) \/ (A ^^ C) = A ^^ (B \/ C) & (B ^^ A) \/ (C ^^ A) = (B \/ C) ^^ A ) by A1, A5, A9, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th21: :: FLANG_1:21 for E being set for A, B, C being Subset of (E ^omega) holds ( (A ^^ B) \ (A ^^ C) c= A ^^ (B \ C) & (B ^^ A) \ (C ^^ A) c= (B \ C) ^^ A ) proof let E be set ; ::_thesis: for A, B, C being Subset of (E ^omega) holds ( (A ^^ B) \ (A ^^ C) c= A ^^ (B \ C) & (B ^^ A) \ (C ^^ A) c= (B \ C) ^^ A ) let A, B, C be Subset of (E ^omega); ::_thesis: ( (A ^^ B) \ (A ^^ C) c= A ^^ (B \ C) & (B ^^ A) \ (C ^^ A) c= (B \ C) ^^ A ) thus (A ^^ B) \ (A ^^ C) c= A ^^ (B \ C) ::_thesis: (B ^^ A) \ (C ^^ A) c= (B \ C) ^^ A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A ^^ B) \ (A ^^ C) or x in A ^^ (B \ C) ) assume A1: x in (A ^^ B) \ (A ^^ C) ; ::_thesis: x in A ^^ (B \ C) then x in A ^^ B by XBOOLE_0:def_5; then consider a, b being Element of E ^omega such that A2: a in A and A3: b in B and A4: x = a ^ b by Def1; A5: now__::_thesis:_(_not_b_in_C_implies_x_in_A_^^_(B_\_C)_) assume not b in C ; ::_thesis: x in A ^^ (B \ C) then b in B \ C by A3, XBOOLE_0:def_5; hence x in A ^^ (B \ C) by A2, A4, Def1; ::_thesis: verum end; not x in A ^^ C by A1, XBOOLE_0:def_5; hence x in A ^^ (B \ C) by A2, A4, A5, Def1; ::_thesis: verum end; thus (B ^^ A) \ (C ^^ A) c= (B \ C) ^^ A ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (B ^^ A) \ (C ^^ A) or x in (B \ C) ^^ A ) assume A6: x in (B ^^ A) \ (C ^^ A) ; ::_thesis: x in (B \ C) ^^ A then x in B ^^ A by XBOOLE_0:def_5; then consider b, a being Element of E ^omega such that A7: b in B and A8: ( a in A & x = b ^ a ) by Def1; A9: now__::_thesis:_(_not_b_in_C_implies_x_in_(B_\_C)_^^_A_) assume not b in C ; ::_thesis: x in (B \ C) ^^ A then b in B \ C by A7, XBOOLE_0:def_5; hence x in (B \ C) ^^ A by A8, Def1; ::_thesis: verum end; not x in C ^^ A by A6, XBOOLE_0:def_5; hence x in (B \ C) ^^ A by A8, A9, Def1; ::_thesis: verum end; end; theorem :: FLANG_1:22 for E being set for A, B, C being Subset of (E ^omega) holds ( (A ^^ B) \+\ (A ^^ C) c= A ^^ (B \+\ C) & (B ^^ A) \+\ (C ^^ A) c= (B \+\ C) ^^ A ) proof let E be set ; ::_thesis: for A, B, C being Subset of (E ^omega) holds ( (A ^^ B) \+\ (A ^^ C) c= A ^^ (B \+\ C) & (B ^^ A) \+\ (C ^^ A) c= (B \+\ C) ^^ A ) let A, B, C be Subset of (E ^omega); ::_thesis: ( (A ^^ B) \+\ (A ^^ C) c= A ^^ (B \+\ C) & (B ^^ A) \+\ (C ^^ A) c= (B \+\ C) ^^ A ) (A ^^ B) \+\ (A ^^ C) = ((A ^^ B) \/ (A ^^ C)) \ ((A ^^ B) /\ (A ^^ C)) by XBOOLE_1:101 .= (A ^^ (B \/ C)) \ ((A ^^ B) /\ (A ^^ C)) by Th20 ; then A1: (A ^^ B) \+\ (A ^^ C) c= (A ^^ (B \/ C)) \ (A ^^ (B /\ C)) by Th19, XBOOLE_1:34; (B ^^ A) \+\ (C ^^ A) = ((B ^^ A) \/ (C ^^ A)) \ ((B ^^ A) /\ (C ^^ A)) by XBOOLE_1:101 .= ((B \/ C) ^^ A) \ ((B ^^ A) /\ (C ^^ A)) by Th20 ; then A2: (B ^^ A) \+\ (C ^^ A) c= ((B \/ C) ^^ A) \ ((B /\ C) ^^ A) by Th19, XBOOLE_1:34; ((B \/ C) ^^ A) \ ((B /\ C) ^^ A) c= ((B \/ C) \ (B /\ C)) ^^ A by Th21; then A3: (B ^^ A) \+\ (C ^^ A) c= ((B \/ C) \ (B /\ C)) ^^ A by A2, XBOOLE_1:1; (A ^^ (B \/ C)) \ (A ^^ (B /\ C)) c= A ^^ ((B \/ C) \ (B /\ C)) by Th21; then (A ^^ B) \+\ (A ^^ C) c= A ^^ ((B \/ C) \ (B /\ C)) by A1, XBOOLE_1:1; hence ( (A ^^ B) \+\ (A ^^ C) c= A ^^ (B \+\ C) & (B ^^ A) \+\ (C ^^ A) c= (B \+\ C) ^^ A ) by A3, XBOOLE_1:101; ::_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) means :Def2: :: FLANG_1:def 2 ex concat being Function of NAT,(bool (E ^omega)) st ( it = concat . n & concat . 0 = {(<%> E)} & ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) ); existence ex b1 being Subset of (E ^omega) ex concat being Function of NAT,(bool (E ^omega)) st ( b1 = concat . n & concat . 0 = {(<%> E)} & ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) ) proof defpred S1[ set , set , set ] means ex B, C being Subset of (E ^omega) st ( C = $3 & B = $2 & C = B ^^ A ); A1: for i being Element of NAT for x being Element of bool (E ^omega) ex y being Element of bool (E ^omega) st S1[i,x,y] proof let i be Element of NAT ; ::_thesis: for x being Element of bool (E ^omega) ex y being Element of bool (E ^omega) st S1[i,x,y] let x be Element of bool (E ^omega); ::_thesis: ex y being Element of bool (E ^omega) st S1[i,x,y] take x ^^ A ; ::_thesis: S1[i,x,x ^^ A] thus S1[i,x,x ^^ A] ; ::_thesis: verum end; consider f being Function of NAT,(bool (E ^omega)) such that A2: ( f . 0 = {(<%> E)} & ( for i being Element of NAT holds S1[i,f . i,f . (i + 1)] ) ) from RECDEF_1:sch_2(A1); consider C being Subset of (E ^omega) such that A3: C = f . n ; take C ; ::_thesis: ex concat being Function of NAT,(bool (E ^omega)) st ( C = concat . n & concat . 0 = {(<%> E)} & ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) ) now__::_thesis:_for_i_being_Nat_holds_f_._(i_+_1)_=_(f_._i)_^^_A let i be Nat; ::_thesis: f . (i + 1) = (f . i) ^^ A reconsider j = i as Element of NAT by ORDINAL1:def_12; ex B, C being Subset of (E ^omega) st ( C = f . (j + 1) & B = f . j & C = B ^^ A ) by A2; hence f . (i + 1) = (f . i) ^^ A ; ::_thesis: verum end; hence ex concat being Function of NAT,(bool (E ^omega)) st ( C = concat . n & concat . 0 = {(<%> E)} & ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) ) by A2, A3; ::_thesis: verum end; uniqueness for b1, b2 being Subset of (E ^omega) st ex concat being Function of NAT,(bool (E ^omega)) st ( b1 = concat . n & concat . 0 = {(<%> E)} & ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) ) & ex concat being Function of NAT,(bool (E ^omega)) st ( b2 = concat . n & concat . 0 = {(<%> E)} & ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) ) holds b1 = b2 proof let C1, C2 be Subset of (E ^omega); ::_thesis: ( ex concat being Function of NAT,(bool (E ^omega)) st ( C1 = concat . n & concat . 0 = {(<%> E)} & ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) ) & ex concat being Function of NAT,(bool (E ^omega)) st ( C2 = concat . n & concat . 0 = {(<%> E)} & ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) ) implies C1 = C2 ) given f1 being Function of NAT,(bool (E ^omega)) such that A4: C1 = f1 . n and A5: f1 . 0 = {(<%> E)} and A6: for i being Nat holds f1 . (i + 1) = (f1 . i) ^^ A ; ::_thesis: ( for concat being Function of NAT,(bool (E ^omega)) holds ( not C2 = concat . n or not concat . 0 = {(<%> E)} or ex i being Nat st not concat . (i + 1) = (concat . i) ^^ A ) or C1 = C2 ) given f2 being Function of NAT,(bool (E ^omega)) such that A7: C2 = f2 . n and A8: f2 . 0 = {(<%> E)} and A9: for i being Nat holds f2 . (i + 1) = (f2 . i) ^^ A ; ::_thesis: C1 = C2 defpred S1[ Nat] means f1 . $1 = f2 . $1; A10: 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 A11: S1[k] ; ::_thesis: S1[k + 1] f2 . (k + 1) = (f2 . k) ^^ A by A9; hence S1[k + 1] by A6, A11; ::_thesis: verum end; A12: S1[ 0 ] by A5, A8; for k being Nat holds S1[k] from NAT_1:sch_2(A12, A10); hence C1 = C2 by A4, A7; ::_thesis: verum end; end; :: deftheorem Def2 defines |^ FLANG_1:def_2_:_ for E being set for A being Subset of (E ^omega) for n being Nat for b4 being Subset of (E ^omega) holds ( b4 = A |^ n iff ex concat being Function of NAT,(bool (E ^omega)) st ( b4 = concat . n & concat . 0 = {(<%> E)} & ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) ) ); theorem Th23: :: FLANG_1:23 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 consider concat being Function of NAT,(bool (E ^omega)) such that A1: A |^ n = concat . n and A2: concat . 0 = {(<%> E)} and A3: for i being Nat holds concat . (i + 1) = (concat . i) ^^ A by Def2; concat . (n + 1) = (A |^ n) ^^ A by A1, A3; hence A |^ (n + 1) = (A |^ n) ^^ A by A2, A3, Def2; ::_thesis: verum end; theorem Th24: :: FLANG_1:24 for E being set for A being Subset of (E ^omega) holds A |^ 0 = {(<%> E)} proof let E be set ; ::_thesis: for A being Subset of (E ^omega) holds A |^ 0 = {(<%> E)} let A be Subset of (E ^omega); ::_thesis: A |^ 0 = {(<%> E)} ex concat being Function of NAT,(bool (E ^omega)) st ( A |^ 0 = concat . 0 & concat . 0 = {(<%> E)} & ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) ) by Def2; hence A |^ 0 = {(<%> E)} ; ::_thesis: verum end; theorem Th25: :: FLANG_1:25 for E being set for A being Subset of (E ^omega) holds A |^ 1 = A proof let E be set ; ::_thesis: for A being Subset of (E ^omega) holds A |^ 1 = A let A be Subset of (E ^omega); ::_thesis: A |^ 1 = A consider concat being Function of NAT,(bool (E ^omega)) such that A1: A |^ 1 = concat . 1 and A2: ( concat . 0 = {(<%> E)} & ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) ) by Def2; thus A |^ 1 = concat . (0 + 1) by A1 .= {(<%> E)} ^^ A by A2 .= A by Th13 ; ::_thesis: verum end; theorem Th26: :: FLANG_1:26 for E being set for A being Subset of (E ^omega) holds A |^ 2 = A ^^ A proof let E be set ; ::_thesis: for A being Subset of (E ^omega) holds A |^ 2 = A ^^ A let A be Subset of (E ^omega); ::_thesis: A |^ 2 = A ^^ A thus A |^ 2 = A |^ (1 + 1) .= (A |^ 1) ^^ A by Th23 .= A ^^ A by Th25 ; ::_thesis: verum end; theorem Th27: :: FLANG_1:27 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 = {} ) ) defpred S1[ Nat] means A |^ $1 = {} ; thus ( A |^ n = {} implies ( n > 0 & A = {} ) ) ::_thesis: ( n > 0 & A = {} implies A |^ n = {} ) proof assume that A1: A |^ n = {} and A2: ( n <= 0 or A <> {} ) ; ::_thesis: contradiction A3: now__::_thesis:_not_A_<>_{} defpred S2[ Nat] means A |^ $1 <> {} ; assume A4: A <> {} ; ::_thesis: contradiction A5: now__::_thesis:_for_n_being_Nat_st_S2[n]_holds_ S2[n_+_1] let n be Nat; ::_thesis: ( S2[n] implies S2[n + 1] ) assume S2[n] ; ::_thesis: S2[n + 1] then consider a1 being Element of E ^omega such that A6: a1 in A |^ n by SUBSET_1:4; consider a2 being Element of E ^omega such that A7: a2 in A by A4, SUBSET_1:4; a1 ^ a2 in (A |^ n) ^^ A by A6, A7, Def1; hence S2[n + 1] by Th23; ::_thesis: verum end; A |^ 0 = {(<%> E)} by Th24; then A8: S2[ 0 ] ; for n being Nat holds S2[n] from NAT_1:sch_2(A8, A5); hence contradiction by A1; ::_thesis: verum end; now__::_thesis:_not_n_<=_0 assume n <= 0 ; ::_thesis: contradiction then n = 0 ; then A |^ n = {(<%> E)} by Th24; hence contradiction by A1; ::_thesis: verum end; hence contradiction by A2, A3; ::_thesis: verum end; assume that A9: n > 0 and A10: A = {} ; ::_thesis: A |^ n = {} A11: now__::_thesis:_for_m_being_Nat_st_1_<=_m_&_S1[m]_holds_ S1[m_+_1] let m be Nat; ::_thesis: ( 1 <= m & S1[m] implies S1[m + 1] ) assume that 1 <= m and S1[m] ; ::_thesis: S1[m + 1] ({} (E ^omega)) |^ (m + 1) = (({} (E ^omega)) |^ m) ^^ ({} (E ^omega)) by Th23 .= {} by Th12 ; hence S1[m + 1] by A10; ::_thesis: verum end; A12: S1[1] by A10, Th25; A13: for m being Nat st m >= 1 holds S1[m] from NAT_1:sch_8(A12, A11); n >= 0 + 1 by A9, NAT_1:13; hence A |^ n = {} by A13; ::_thesis: verum end; theorem Th28: :: FLANG_1:28 for E being set for n being Nat holds {(<%> E)} |^ n = {(<%> E)} proof let E be set ; ::_thesis: for n being Nat holds {(<%> E)} |^ n = {(<%> E)} let n be Nat; ::_thesis: {(<%> E)} |^ n = {(<%> E)} defpred S1[ Nat] means {(<%> E)} |^ $1 = {(<%> E)}; 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] {(<%> E)} |^ (n + 1) = ({(<%> E)} |^ n) ^^ {(<%> E)} by Th23 .= {(<%> E)} by A2, Th13 ; hence S1[n + 1] ; ::_thesis: verum end; A3: S1[ 0 ] by Th24; for n being Nat holds S1[n] from NAT_1:sch_2(A3, A1); hence {(<%> E)} |^ n = {(<%> E)} ; ::_thesis: verum end; theorem :: FLANG_1:29 for E being set for A being Subset of (E ^omega) for n being Nat holds ( A |^ n = {(<%> E)} iff ( n = 0 or A = {(<%> E)} ) ) proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for n being Nat holds ( A |^ n = {(<%> E)} iff ( n = 0 or A = {(<%> E)} ) ) let A be Subset of (E ^omega); ::_thesis: for n being Nat holds ( A |^ n = {(<%> E)} iff ( n = 0 or A = {(<%> E)} ) ) let n be Nat; ::_thesis: ( A |^ n = {(<%> E)} iff ( n = 0 or A = {(<%> E)} ) ) thus ( not A |^ n = {(<%> E)} or n = 0 or A = {(<%> E)} ) ::_thesis: ( ( n = 0 or A = {(<%> E)} ) implies A |^ n = {(<%> E)} ) proof assume A1: A |^ n = {(<%> E)} ; ::_thesis: ( n = 0 or A = {(<%> E)} ) now__::_thesis:_(_n_>_0_implies_A_=_{(<%>_E)}_) assume n > 0 ; ::_thesis: A = {(<%> E)} then consider m being Nat such that A2: m + 1 = n by NAT_1:6; A |^ n = (A |^ m) ^^ A by A2, Th23; hence A = {(<%> E)} by A1, Th14; ::_thesis: verum end; hence ( n = 0 or A = {(<%> E)} ) ; ::_thesis: verum end; assume ( n = 0 or A = {(<%> E)} ) ; ::_thesis: A |^ n = {(<%> E)} hence A |^ n = {(<%> E)} by Th24, Th28; ::_thesis: verum end; theorem Th30: :: FLANG_1:30 for E being set for A being Subset of (E ^omega) for n being Nat st <%> E in A holds <%> E in A |^ n proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for n being Nat st <%> E in A holds <%> E in A |^ n let A be Subset of (E ^omega); ::_thesis: for n being Nat st <%> E in A holds <%> E in A |^ n let n be Nat; ::_thesis: ( <%> E in A implies <%> E in A |^ n ) defpred S1[ Nat] means <%> E in A |^ $1; assume A1: <%> E in A ; ::_thesis: <%> E in A |^ n A2: 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 S1[n] ; ::_thesis: S1[n + 1] then <%> E in (A |^ n) ^^ A by A1, Th15; hence S1[n + 1] by Th23; ::_thesis: verum end; A |^ 0 = {(<%> E)} by Th24; then A3: S1[ 0 ] by TARSKI:def_1; for n being Nat holds S1[n] from NAT_1:sch_2(A3, A2); hence <%> E in A |^ n ; ::_thesis: verum end; theorem :: FLANG_1:31 for E being set for A being Subset of (E ^omega) for n being Nat st <%> E in A |^ n & n > 0 holds <%> E in A proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for n being Nat st <%> E in A |^ n & n > 0 holds <%> E in A let A be Subset of (E ^omega); ::_thesis: for n being Nat st <%> E in A |^ n & n > 0 holds <%> E in A let n be Nat; ::_thesis: ( <%> E in A |^ n & n > 0 implies <%> E in A ) assume that A1: <%> E in A |^ n and A2: n > 0 ; ::_thesis: <%> E in A consider m being Nat such that A3: m + 1 = n by A2, NAT_1:6; A |^ n = (A |^ m) ^^ A by A3, Th23; then ex a1, a2 being Element of E ^omega st ( a1 in A |^ m & a2 in A & a1 ^ a2 = <%> E ) by A1, Def1; hence <%> E in A by AFINSQ_1:30; ::_thesis: verum end; theorem Th32: :: FLANG_1:32 for E being set for A being Subset of (E ^omega) for n being Nat holds (A |^ n) ^^ A = A ^^ (A |^ n) proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for n being Nat holds (A |^ n) ^^ A = A ^^ (A |^ n) let A be Subset of (E ^omega); ::_thesis: for n being Nat holds (A |^ n) ^^ A = A ^^ (A |^ n) let n be Nat; ::_thesis: (A |^ n) ^^ A = A ^^ (A |^ n) defpred S1[ Nat] means (A |^ $1) ^^ A = A ^^ (A |^ $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 |^ (n + 1)) ^^ A = ((A |^ n) ^^ A) ^^ A by Th23 .= A ^^ ((A |^ n) ^^ A) by A2, Th18 .= A ^^ (A |^ (n + 1)) by Th23 ; hence S1[n + 1] ; ::_thesis: verum end; (A |^ 0) ^^ A = {(<%> E)} ^^ A by Th24 .= A by Th13 .= A ^^ {(<%> E)} by Th13 .= A ^^ (A |^ 0) by Th24 ; then A3: S1[ 0 ] ; for n being Nat holds S1[n] from NAT_1:sch_2(A3, A1); hence (A |^ n) ^^ A = A ^^ (A |^ n) ; ::_thesis: verum end; theorem Th33: :: FLANG_1:33 for E being set for A being Subset of (E ^omega) for m, n being Nat holds A |^ (m + n) = (A |^ m) ^^ (A |^ n) proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for m, n being Nat holds A |^ (m + n) = (A |^ m) ^^ (A |^ n) let A be Subset of (E ^omega); ::_thesis: for m, n being Nat holds A |^ (m + n) = (A |^ m) ^^ (A |^ n) let m, n be Nat; ::_thesis: A |^ (m + n) = (A |^ m) ^^ (A |^ n) defpred S1[ Nat] means for m, n being Nat st m + n <= $1 holds A |^ (m + n) = (A |^ m) ^^ (A |^ n); A1: now__::_thesis:_for_l_being_Nat_st_S1[l]_holds_ S1[l_+_1] let l be Nat; ::_thesis: ( S1[l] implies S1[l + 1] ) assume A2: S1[l] ; ::_thesis: S1[l + 1] now__::_thesis:_for_m,_n_being_Nat_st_m_+_n_<=_l_+_1_holds_ A_|^_(m_+_n)_=_(A_|^_m)_^^_(A_|^_n) let m, n be Nat; ::_thesis: ( m + n <= l + 1 implies A |^ (m + n) = (A |^ m) ^^ (A |^ n) ) A3: now__::_thesis:_(_m_+_n_<_l_+_1_implies_A_|^_(m_+_n)_=_(A_|^_m)_^^_(A_|^_n)_) assume m + n < l + 1 ; ::_thesis: A |^ (m + n) = (A |^ m) ^^ (A |^ n) then m + n <= l by NAT_1:13; hence A |^ (m + n) = (A |^ m) ^^ (A |^ n) by A2; ::_thesis: verum end; A4: now__::_thesis:_(_m_+_n_=_l_+_1_implies_A_|^_(m_+_n)_=_(A_|^_m)_^^_(A_|^_n)_) assume A5: m + n = l + 1 ; ::_thesis: A |^ (m + n) = (A |^ m) ^^ (A |^ n) A6: now__::_thesis:_(_n_=_0_implies_A_|^_(m_+_n)_=_(A_|^_m)_^^_(A_|^_n)_) assume A7: n = 0 ; ::_thesis: A |^ (m + n) = (A |^ m) ^^ (A |^ n) thus A |^ (m + n) = (A |^ (l + 1)) ^^ {(<%> E)} by A5, Th13 .= (A |^ m) ^^ (A |^ n) by A5, A7, Th24 ; ::_thesis: verum end; A8: now__::_thesis:_(_m_>_0_&_n_>_0_implies_A_|^_(m_+_n)_=_(A_|^_m)_^^_(A_|^_n)_) assume that A9: m > 0 and A10: n > 0 ; ::_thesis: A |^ (m + n) = (A |^ m) ^^ (A |^ n) consider k being Nat such that A11: k + 1 = m by A9, NAT_1:6; A |^ (m + n) = A |^ ((k + n) + 1) by A11 .= (A |^ (k + n)) ^^ A by Th23 .= A ^^ (A |^ (k + n)) by Th32 .= A ^^ ((A |^ k) ^^ (A |^ n)) by A2, A5, A11 .= (A ^^ (A |^ k)) ^^ (A |^ n) by Th18 .= ((A |^ k) ^^ A) ^^ (A |^ n) by Th32 .= ((A |^ k) ^^ (A |^ 1)) ^^ (A |^ n) by Th25 .= (A |^ m) ^^ (A |^ n) by A2, A5, A10, A11, Th2 ; hence A |^ (m + n) = (A |^ m) ^^ (A |^ n) ; ::_thesis: verum end; now__::_thesis:_(_m_=_0_implies_A_|^_(m_+_n)_=_(A_|^_m)_^^_(A_|^_n)_) assume A12: m = 0 ; ::_thesis: A |^ (m + n) = (A |^ m) ^^ (A |^ n) thus A |^ (m + n) = {(<%> E)} ^^ (A |^ (l + 1)) by A5, Th13 .= (A |^ m) ^^ (A |^ n) by A5, A12, Th24 ; ::_thesis: verum end; hence A |^ (m + n) = (A |^ m) ^^ (A |^ n) by A6, A8; ::_thesis: verum end; assume m + n <= l + 1 ; ::_thesis: A |^ (m + n) = (A |^ m) ^^ (A |^ n) hence A |^ (m + n) = (A |^ m) ^^ (A |^ n) by A4, A3, XXREAL_0:1; ::_thesis: verum end; hence S1[l + 1] ; ::_thesis: verum end; A13: S1[ 0 ] proof let m, n be Nat; ::_thesis: ( m + n <= 0 implies A |^ (m + n) = (A |^ m) ^^ (A |^ n) ) assume A14: m + n <= 0 ; ::_thesis: A |^ (m + n) = (A |^ m) ^^ (A |^ n) then A15: m = 0 ; A16: m + n = 0 by A14; hence A |^ (m + n) = (A |^ 0) ^^ {(<%> E)} by Th13 .= (A |^ m) ^^ (A |^ n) by A16, A15, Th24 ; ::_thesis: verum end; for l being Nat holds S1[l] from NAT_1:sch_2(A13, A1); hence A |^ (m + n) = (A |^ m) ^^ (A |^ n) ; ::_thesis: verum end; theorem :: FLANG_1:34 for E being set for A being Subset of (E ^omega) for m, n being Nat holds (A |^ m) |^ n = A |^ (m * n) proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for m, n being Nat holds (A |^ m) |^ n = A |^ (m * n) let A be Subset of (E ^omega); ::_thesis: for m, n being Nat holds (A |^ m) |^ n = A |^ (m * n) let m, n be Nat; ::_thesis: (A |^ m) |^ n = A |^ (m * n) defpred S1[ Nat] means for m, n being Nat st m + n <= $1 holds (A |^ m) |^ n = A |^ (m * n); A1: now__::_thesis:_for_l_being_Nat_st_S1[l]_holds_ S1[l_+_1] let l be Nat; ::_thesis: ( S1[l] implies S1[l + 1] ) assume A2: S1[l] ; ::_thesis: S1[l + 1] now__::_thesis:_for_m,_n_being_Nat_st_m_+_n_<=_l_+_1_holds_ (A_|^_m)_|^_n_=_A_|^_(m_*_n) let m, n be Nat; ::_thesis: ( m + n <= l + 1 implies (A |^ m) |^ n = A |^ (m * n) ) A3: now__::_thesis:_(_m_+_n_<_l_+_1_implies_(A_|^_m)_|^_n_=_A_|^_(m_*_n)_) assume m + n < l + 1 ; ::_thesis: (A |^ m) |^ n = A |^ (m * n) then m + n <= l by NAT_1:13; hence (A |^ m) |^ n = A |^ (m * n) by A2; ::_thesis: verum end; A4: now__::_thesis:_(_m_+_n_=_l_+_1_implies_(A_|^_m)_|^_n_=_A_|^_(m_*_n)_) assume A5: m + n = l + 1 ; ::_thesis: (A |^ m) |^ n = A |^ (m * n) A6: now__::_thesis:_(_m_>_0_&_n_>_0_implies_(A_|^_m)_|^_n_=_A_|^_(m_*_n)_) assume that m > 0 and A7: n > 0 ; ::_thesis: (A |^ m) |^ n = A |^ (m * n) consider k being Nat such that A8: k + 1 = n by A7, NAT_1:6; A9: m + k <= l by A5, A8; (A |^ m) |^ n = ((A |^ m) |^ k) ^^ (A |^ m) by A8, Th23 .= (A |^ (m * k)) ^^ (A |^ m) by A2, A9 .= A |^ ((m * k) + m) by Th33 .= A |^ (m * n) by A8 ; hence (A |^ m) |^ n = A |^ (m * n) ; ::_thesis: verum end; A10: now__::_thesis:_(_n_=_0_implies_(A_|^_m)_|^_n_=_A_|^_(m_*_n)_) assume A11: n = 0 ; ::_thesis: (A |^ m) |^ n = A |^ (m * n) hence (A |^ m) |^ n = {(<%> E)} by Th24 .= A |^ (m * n) by A11, Th24 ; ::_thesis: verum end; now__::_thesis:_(_m_=_0_implies_(A_|^_m)_|^_n_=_A_|^_(m_*_n)_) assume A12: m = 0 ; ::_thesis: (A |^ m) |^ n = A |^ (m * n) hence (A |^ m) |^ n = {(<%> E)} |^ n by Th24 .= {(<%> E)} by Th28 .= A |^ (m * n) by A12, Th24 ; ::_thesis: verum end; hence (A |^ m) |^ n = A |^ (m * n) by A10, A6; ::_thesis: verum end; assume m + n <= l + 1 ; ::_thesis: (A |^ m) |^ n = A |^ (m * n) hence (A |^ m) |^ n = A |^ (m * n) by A4, A3, XXREAL_0:1; ::_thesis: verum end; hence S1[l + 1] ; ::_thesis: verum end; A13: S1[ 0 ] proof let m, n be Nat; ::_thesis: ( m + n <= 0 implies (A |^ m) |^ n = A |^ (m * n) ) assume A14: m + n <= 0 ; ::_thesis: (A |^ m) |^ n = A |^ (m * n) then A15: m = 0 ; n = 0 by A14; hence (A |^ m) |^ n = {(<%> E)} by Th24 .= A |^ (m * n) by A15, Th24 ; ::_thesis: verum end; A16: for l being Nat holds S1[l] from NAT_1:sch_2(A13, A1); now__::_thesis:_for_m,_n_being_Nat_holds_(A_|^_m)_|^_n_=_A_|^_(m_*_n) let m, n be Nat; ::_thesis: (A |^ m) |^ n = A |^ (m * n) reconsider l = m + n as Nat ; m + n <= l ; hence (A |^ m) |^ n = A |^ (m * n) by A16; ::_thesis: verum end; hence (A |^ m) |^ n = A |^ (m * n) ; ::_thesis: verum end; theorem Th35: :: FLANG_1:35 for E being set for A being Subset of (E ^omega) for n being Nat st <%> E in A & n > 0 holds A c= A |^ n proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for n being Nat st <%> E in A & n > 0 holds A c= A |^ n let A be Subset of (E ^omega); ::_thesis: for n being Nat st <%> E in A & n > 0 holds A c= A |^ n let n be Nat; ::_thesis: ( <%> E in A & n > 0 implies A c= A |^ n ) assume that A1: <%> E in A and A2: n > 0 ; ::_thesis: A c= A |^ n consider m being Nat such that A3: m + 1 = n by A2, NAT_1:6; <%> E in A |^ m by A1, Th30; then A c= (A |^ m) ^^ A by Th16; hence A c= A |^ n by A3, Th23; ::_thesis: verum end; theorem :: FLANG_1:36 for E being set for A being Subset of (E ^omega) for m, n being Nat st <%> E in A & 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 <%> E in A & m > n holds A |^ n c= A |^ m let A be Subset of (E ^omega); ::_thesis: for m, n being Nat st <%> E in A & m > n holds A |^ n c= A |^ m let m, n be Nat; ::_thesis: ( <%> E in A & m > n implies A |^ n c= A |^ m ) assume that A1: <%> E in A and A2: m > n ; ::_thesis: A |^ n c= A |^ m consider k being Nat such that A3: n + k = m by A2, NAT_1:10; <%> E in A |^ k by A1, Th30; then A |^ n c= (A |^ k) ^^ (A |^ n) by Th16; hence A |^ n c= A |^ m by A3, Th33; ::_thesis: verum end; theorem Th37: :: FLANG_1:37 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 ) defpred S1[ Nat] means A |^ $1 c= B |^ $1; assume A1: A c= B ; ::_thesis: A |^ n c= B |^ n A2: 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 A3: S1[n] ; ::_thesis: S1[n + 1] ( (A |^ n) ^^ A = A |^ (n + 1) & (B |^ n) ^^ B = B |^ (n + 1) ) by Th23; hence S1[n + 1] by A1, A3, Th17; ::_thesis: verum end; A |^ 0 = {(<%> E)} by Th24; then A4: S1[ 0 ] by Th24; for n being Nat holds S1[n] from NAT_1:sch_2(A4, A2); hence A |^ n c= B |^ n ; ::_thesis: verum end; theorem :: FLANG_1:38 for E being set for A, B being Subset of (E ^omega) for n being Nat holds (A |^ n) \/ (B |^ n) c= (A \/ B) |^ n proof let E be set ; ::_thesis: for A, B being Subset of (E ^omega) for n being Nat holds (A |^ n) \/ (B |^ n) c= (A \/ B) |^ n let A, B be Subset of (E ^omega); ::_thesis: for n being Nat holds (A |^ n) \/ (B |^ n) c= (A \/ B) |^ n let n be Nat; ::_thesis: (A |^ n) \/ (B |^ n) c= (A \/ B) |^ n ( A |^ n c= (A \/ B) |^ n & B |^ n c= (A \/ B) |^ n ) by Th37, XBOOLE_1:7; hence (A |^ n) \/ (B |^ n) c= (A \/ B) |^ n by XBOOLE_1:8; ::_thesis: verum end; theorem :: FLANG_1:39 for E being set for A, B being Subset of (E ^omega) for n being Nat holds (A /\ B) |^ n c= (A |^ n) /\ (B |^ n) proof let E be set ; ::_thesis: for A, B being Subset of (E ^omega) for n being Nat holds (A /\ B) |^ n c= (A |^ n) /\ (B |^ n) let A, B be Subset of (E ^omega); ::_thesis: for n being Nat holds (A /\ B) |^ n c= (A |^ n) /\ (B |^ n) let n be Nat; ::_thesis: (A /\ B) |^ n c= (A |^ n) /\ (B |^ n) ( (A /\ B) |^ n c= A |^ n & (A /\ B) |^ n c= B |^ n ) by Th37, XBOOLE_1:17; hence (A /\ B) |^ n c= (A |^ n) /\ (B |^ n) by XBOOLE_1:19; ::_thesis: verum end; theorem Th40: :: FLANG_1:40 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 ( a in C |^ m & b in C |^ n ) ; ::_thesis: a ^ b in C |^ (m + n) then a ^ b in (C |^ m) ^^ (C |^ n) by Def1; hence a ^ b in C |^ (m + n) by Th33; ::_thesis: verum end; begin definition let E be set ; let A be Subset of (E ^omega); funcA * -> Subset of (E ^omega) equals :: FLANG_1:def 3 union { B where B is Subset of (E ^omega) : ex n being Nat st B = A |^ n } ; coherence union { B where B is Subset of (E ^omega) : ex n being Nat st B = A |^ n } is Subset of (E ^omega) proof defpred S1[ set ] means ex n being Nat st $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 B = A |^ n } is Subset of (E ^omega) ; ::_thesis: verum end; end; :: deftheorem defines * FLANG_1:def_3_:_ 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 B = A |^ n } ; theorem Th41: :: FLANG_1:41 for E, x being set for A being Subset of (E ^omega) holds ( x in A * iff ex n being Nat st 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 x in A |^ n ) let A be Subset of (E ^omega); ::_thesis: ( x in A * iff ex n being Nat st x in A |^ n ) thus ( x in A * implies ex n being Nat st x in A |^ n ) ::_thesis: ( ex n being Nat st x in A |^ n implies x in A * ) proof defpred S1[ set ] means ex k being Nat st $1 = A |^ k; assume x in A * ; ::_thesis: ex n being Nat st 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 k being Nat st B = A |^ k } by TARSKI:def_4; A3: X in { B where B is Subset of (E ^omega) : S1[B] } by A2; S1[X] from CARD_FIL:sch_1(A3); hence ex n being Nat st x in A |^ n by A1; ::_thesis: verum end; given n being Nat such that A4: x in A |^ n ; ::_thesis: x in A * defpred S1[ set ] means ex k being Nat st $1 = A |^ k; consider B being Subset of (E ^omega) such that A5: x in B and A6: S1[B] by A4; reconsider A = { C where C is Subset of (E ^omega) : S1[C] } as Subset-Family of (E ^omega) from DOMAIN_1:sch_7(); B in A by A6; hence x in A * by A5, TARSKI:def_4; ::_thesis: verum end; theorem Th42: :: FLANG_1:42 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 * A |^ n in { B where B is Subset of (E ^omega) : ex k being Nat st B = A |^ k } ; hence A |^ n c= A * by ZFMISC_1:74; ::_thesis: verum end; theorem Th43: :: FLANG_1:43 for E being set for A being Subset of (E ^omega) holds A c= A * proof let E be set ; ::_thesis: for A being Subset of (E ^omega) holds A c= A * let A be Subset of (E ^omega); ::_thesis: A c= A * A = A |^ 1 by Th25; hence A c= A * by Th42; ::_thesis: verum end; theorem :: FLANG_1:44 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 Th26; hence A ^^ A c= A * by Th42; ::_thesis: verum end; theorem Th45: :: FLANG_1:45 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 k being Nat such that A3: a in C |^ k by A1, Th41; consider l being Nat such that A4: b in C |^ l by A2, Th41; a ^ b in C |^ (k + l) by A3, A4, Th40; hence a ^ b in C * by Th41; ::_thesis: verum end; theorem Th46: :: FLANG_1:46 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 A1: ( A c= C * & B c= C * ) ; ::_thesis: A ^^ B c= C * thus A ^^ B c= C * ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A ^^ B or 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 Def1; hence x in C * by A1, Th45; ::_thesis: verum end; end; theorem :: FLANG_1:47 for E being set for A being Subset of (E ^omega) holds ( A * = {(<%> E)} iff ( A = {} or A = {(<%> E)} ) ) proof let E be set ; ::_thesis: for A being Subset of (E ^omega) holds ( A * = {(<%> E)} iff ( A = {} or A = {(<%> E)} ) ) let A be Subset of (E ^omega); ::_thesis: ( A * = {(<%> E)} iff ( A = {} or A = {(<%> E)} ) ) thus ( not A * = {(<%> E)} or A = {} or A = {(<%> E)} ) ::_thesis: ( ( A = {} or A = {(<%> E)} ) implies A * = {(<%> E)} ) proof A1: A c= A * by Th43; assume that A2: A * = {(<%> E)} and A3: ( A <> {} & A <> {(<%> E)} ) ; ::_thesis: contradiction ex x being set st ( x in A & x <> <%> E ) by A3, ZFMISC_1:35; hence contradiction by A2, A1, TARSKI:def_1; ::_thesis: verum end; A4: now__::_thesis:_(_A_=_{}_implies_A_*_=_{(<%>_E)}_) assume A5: A = {} ; ::_thesis: A * = {(<%> E)} A6: now__::_thesis:_for_x_being_set_st_x_in_A_*_holds_ x_in_{(<%>_E)} let x be set ; ::_thesis: ( x in A * implies x in {(<%> E)} ) assume x in A * ; ::_thesis: x in {(<%> E)} then consider n being Nat such that A7: x in A |^ n by Th41; ( n = 0 implies x in {(<%> E)} ) by A7, Th24; hence x in {(<%> E)} by A5, A7, Th27; ::_thesis: verum end; now__::_thesis:_for_x_being_set_st_x_in_{(<%>_E)}_holds_ x_in_A_* let x be set ; ::_thesis: ( x in {(<%> E)} implies x in A * ) assume x in {(<%> E)} ; ::_thesis: x in A * then x in A |^ 0 by Th24; hence x in A * by Th41; ::_thesis: verum end; hence A * = {(<%> E)} by A6, TARSKI:1; ::_thesis: verum end; now__::_thesis:_(_A_=_{(<%>_E)}_implies_A_*_=_{(<%>_E)}_) assume A8: A = {(<%> E)} ; ::_thesis: A * = {(<%> E)} A9: A * c= {(<%> E)} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A * or x in {(<%> E)} ) assume x in A * ; ::_thesis: x in {(<%> E)} then ex n being Nat st x in A |^ n by Th41; hence x in {(<%> E)} by A8, Th28; ::_thesis: verum end; {(<%> E)} c= A * proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(<%> E)} or x in A * ) assume x in {(<%> E)} ; ::_thesis: x in A * then x in A |^ 0 by Th24; hence x in A * by Th41; ::_thesis: verum end; hence A * = {(<%> E)} by A9, XBOOLE_0:def_10; ::_thesis: verum end; hence ( ( A = {} or A = {(<%> E)} ) implies A * = {(<%> E)} ) by A4; ::_thesis: verum end; theorem Th48: :: FLANG_1:48 for E being set for A being Subset of (E ^omega) holds <%> E in A * proof let E be set ; ::_thesis: for A being Subset of (E ^omega) holds <%> E in A * let A be Subset of (E ^omega); ::_thesis: <%> E in A * {(<%> E)} = A |^ 0 by Th24; then <%> E in A |^ 0 by TARSKI:def_1; hence <%> E in A * by Th41; ::_thesis: verum end; theorem :: FLANG_1:49 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 reconsider a = x as Element of E ^omega by A1, ZFMISC_1:31; x in A * by A1, ZFMISC_1:31; then A3: a ^ a in A * by Th45; a ^ a <> x by A2, Th11; hence contradiction by A1, A3, TARSKI:def_1; ::_thesis: verum end; theorem Th50: :: FLANG_1:50 for E, x being set for A being Subset of (E ^omega) for m being Nat st x in A |^ (m + 1) holds ( x in (A *) ^^ A & x in A ^^ (A *) ) proof let E, x be set ; ::_thesis: for A being Subset of (E ^omega) for m being Nat st x in A |^ (m + 1) holds ( x in (A *) ^^ A & x in A ^^ (A *) ) let A be Subset of (E ^omega); ::_thesis: for m being Nat st x in A |^ (m + 1) holds ( x in (A *) ^^ A & x in A ^^ (A *) ) let m be Nat; ::_thesis: ( x in A |^ (m + 1) implies ( x in (A *) ^^ A & x in A ^^ (A *) ) ) assume x in A |^ (m + 1) ; ::_thesis: ( x in (A *) ^^ A & x in A ^^ (A *) ) then A1: x in (A |^ m) ^^ A by Th23; then consider a, b being Element of E ^omega such that A2: a in A |^ m and A3: ( b in A & x = a ^ b ) by Def1; a in A * by A2, Th41; hence x in (A *) ^^ A by A3, Def1; ::_thesis: x in A ^^ (A *) x in A ^^ (A |^ m) by A1, Th32; then consider a, b being Element of E ^omega such that A4: a in A and A5: b in A |^ m and A6: x = a ^ b by Def1; b in A * by A5, Th41; hence x in A ^^ (A *) by A4, A6, Def1; ::_thesis: verum end; theorem :: FLANG_1:51 for E being set for A being Subset of (E ^omega) for m being Nat holds ( A |^ (m + 1) c= (A *) ^^ A & A |^ (m + 1) c= A ^^ (A *) ) proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for m being Nat holds ( A |^ (m + 1) c= (A *) ^^ A & A |^ (m + 1) c= A ^^ (A *) ) let A be Subset of (E ^omega); ::_thesis: for m being Nat holds ( A |^ (m + 1) c= (A *) ^^ A & A |^ (m + 1) c= A ^^ (A *) ) let m be Nat; ::_thesis: ( A |^ (m + 1) c= (A *) ^^ A & A |^ (m + 1) c= A ^^ (A *) ) thus A |^ (m + 1) c= (A *) ^^ A ::_thesis: A |^ (m + 1) c= A ^^ (A *) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A |^ (m + 1) or x in (A *) ^^ A ) assume x in A |^ (m + 1) ; ::_thesis: x in (A *) ^^ A hence x in (A *) ^^ A by Th50; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A |^ (m + 1) or x in A ^^ (A *) ) assume x in A |^ (m + 1) ; ::_thesis: x in A ^^ (A *) hence x in A ^^ (A *) by Th50; ::_thesis: verum end; theorem Th52: :: FLANG_1:52 for E, x being set for A being Subset of (E ^omega) st ( x in (A *) ^^ A or x in A ^^ (A *) ) holds x in A * proof let E, x be set ; ::_thesis: for A being Subset of (E ^omega) st ( x in (A *) ^^ A or x in A ^^ (A *) ) holds x in A * let A be Subset of (E ^omega); ::_thesis: ( ( x in (A *) ^^ A or x in A ^^ (A *) ) implies x in A * ) A1: now__::_thesis:_for_x_being_set_st_x_in_A_^^_(A_*)_holds_ x_in_A_* let x be set ; ::_thesis: ( x in A ^^ (A *) implies x in A * ) assume x in A ^^ (A *) ; ::_thesis: x in A * then consider a, b being Element of E ^omega such that A2: a in A and A3: b in A * and A4: x = a ^ b by Def1; consider n being Nat such that A5: b in A |^ n by A3, Th41; a in A |^ 1 by A2, Th25; then a ^ b in A |^ (n + 1) by A5, Th40; hence x in A * by A4, Th41; ::_thesis: verum end; now__::_thesis:_for_x_being_set_st_x_in_(A_*)_^^_A_holds_ x_in_A_* let x be set ; ::_thesis: ( x in (A *) ^^ A implies x in A * ) assume x in (A *) ^^ A ; ::_thesis: x in A * then consider a, b being Element of E ^omega such that A6: a in A * and A7: b in A and A8: x = a ^ b by Def1; consider n being Nat such that A9: a in A |^ n by A6, Th41; b in A |^ 1 by A7, Th25; then a ^ b in A |^ (n + 1) by A9, Th40; hence x in A * by A8, Th41; ::_thesis: verum end; hence ( ( x in (A *) ^^ A or x in A ^^ (A *) ) implies x in A * ) by A1; ::_thesis: verum end; theorem :: FLANG_1:53 for E being set for A being Subset of (E ^omega) holds ( (A *) ^^ A c= A * & A ^^ (A *) c= A * ) proof let E be set ; ::_thesis: for A being Subset of (E ^omega) holds ( (A *) ^^ A c= A * & A ^^ (A *) c= A * ) let A be Subset of (E ^omega); ::_thesis: ( (A *) ^^ A c= A * & A ^^ (A *) c= A * ) thus (A *) ^^ A c= A * ::_thesis: A ^^ (A *) c= A * proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A *) ^^ A or x in A * ) assume x in (A *) ^^ A ; ::_thesis: x in A * hence x in A * by Th52; ::_thesis: verum end; thus A ^^ (A *) c= A * ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A ^^ (A *) or x in A * ) assume x in A ^^ (A *) ; ::_thesis: x in A * hence x in A * by Th52; ::_thesis: verum end; end; theorem Th54: :: FLANG_1:54 for E being set for A being Subset of (E ^omega) st <%> E in A holds ( A * = (A *) ^^ A & A * = A ^^ (A *) ) proof let E be set ; ::_thesis: for A being Subset of (E ^omega) st <%> E in A holds ( A * = (A *) ^^ A & A * = A ^^ (A *) ) let A be Subset of (E ^omega); ::_thesis: ( <%> E in A implies ( A * = (A *) ^^ A & A * = A ^^ (A *) ) ) assume A1: <%> E in A ; ::_thesis: ( A * = (A *) ^^ A & A * = A ^^ (A *) ) A2: <%> E in A * by Th48; A3: now__::_thesis:_for_x_being_set_st_x_in_A_*_holds_ (_x_in_(A_*)_^^_A_&_x_in_A_^^_(A_*)_) let x be set ; ::_thesis: ( x in A * implies ( x in (A *) ^^ A & x in A ^^ (A *) ) ) assume x in A * ; ::_thesis: ( x in (A *) ^^ A & x in A ^^ (A *) ) then consider n being Nat such that A4: x in A |^ n by Th41; A5: now__::_thesis:_(_n_=_0_implies_(_x_in_(A_*)_^^_A_&_x_in_A_^^_(A_*)_)_) assume n = 0 ; ::_thesis: ( x in (A *) ^^ A & x in A ^^ (A *) ) then x in {(<%> E)} by A4, Th24; then x = <%> E by TARSKI:def_1; hence ( x in (A *) ^^ A & x in A ^^ (A *) ) by A1, A2, Th15; ::_thesis: verum end; A6: now__::_thesis:_(_n_>_0_implies_x_in_A_^^_(A_*)_) assume n > 0 ; ::_thesis: x in A ^^ (A *) then ex m being Nat st m + 1 = n by NAT_1:6; hence x in A ^^ (A *) by A4, Th50; ::_thesis: verum end; now__::_thesis:_(_n_>_0_implies_x_in_(A_*)_^^_A_) assume n > 0 ; ::_thesis: x in (A *) ^^ A then ex m being Nat st m + 1 = n by NAT_1:6; hence x in (A *) ^^ A by A4, Th50; ::_thesis: verum end; hence ( x in (A *) ^^ A & x in A ^^ (A *) ) by A5, A6; ::_thesis: verum end; then A7: for x being set st x in A * holds x in (A *) ^^ A ; A8: for x being set st x in A * holds x in A ^^ (A *) by A3; for x being set holds ( ( x in (A *) ^^ A implies x in A * ) & ( x in A ^^ (A *) implies x in A * ) ) by Th52; hence ( A * = (A *) ^^ A & A * = A ^^ (A *) ) by A7, A8, TARSKI:1; ::_thesis: verum end; theorem :: FLANG_1:55 for E being set for A being Subset of (E ^omega) for n being Nat st <%> E in A holds ( A * = (A *) ^^ (A |^ n) & A * = (A |^ n) ^^ (A *) ) proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for n being Nat st <%> E in A holds ( A * = (A *) ^^ (A |^ n) & A * = (A |^ n) ^^ (A *) ) let A be Subset of (E ^omega); ::_thesis: for n being Nat st <%> E in A holds ( A * = (A *) ^^ (A |^ n) & A * = (A |^ n) ^^ (A *) ) let n be Nat; ::_thesis: ( <%> E in A implies ( A * = (A *) ^^ (A |^ n) & A * = (A |^ n) ^^ (A *) ) ) defpred S1[ Nat] means ( A * = (A *) ^^ (A |^ $1) & A * = (A |^ $1) ^^ (A *) ); A1: (A |^ 0) ^^ (A *) = {(<%> E)} ^^ (A *) by Th24 .= A * by Th13 ; assume A2: <%> E in A ; ::_thesis: ( A * = (A *) ^^ (A |^ n) & A * = (A |^ n) ^^ (A *) ) 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] A5: (A *) ^^ (A |^ (n + 1)) = (A *) ^^ ((A |^ n) ^^ A) by Th23 .= (A *) ^^ A by A4, Th18 .= A * by A2, Th54 ; (A |^ (n + 1)) ^^ (A *) = ((A |^ n) ^^ A) ^^ (A *) by Th23 .= (A ^^ (A |^ n)) ^^ (A *) by Th32 .= A ^^ (A *) by A4, Th18 .= A * by A2, Th54 ; hence S1[n + 1] by A5; ::_thesis: verum end; (A *) ^^ (A |^ 0) = (A *) ^^ {(<%> E)} by Th24 .= A * by Th13 ; then A6: S1[ 0 ] by A1; for n being Nat holds S1[n] from NAT_1:sch_2(A6, A3); hence ( A * = (A *) ^^ (A |^ n) & A * = (A |^ n) ^^ (A *) ) ; ::_thesis: verum end; theorem Th56: :: FLANG_1:56 for E being set for A being Subset of (E ^omega) holds ( A * = {(<%> E)} \/ (A ^^ (A *)) & A * = {(<%> E)} \/ ((A *) ^^ A) ) proof let E be set ; ::_thesis: for A being Subset of (E ^omega) holds ( A * = {(<%> E)} \/ (A ^^ (A *)) & A * = {(<%> E)} \/ ((A *) ^^ A) ) let A be Subset of (E ^omega); ::_thesis: ( A * = {(<%> E)} \/ (A ^^ (A *)) & A * = {(<%> E)} \/ ((A *) ^^ A) ) A1: now__::_thesis:_for_x_being_set_st_x_in_{(<%>_E)}_\/_((A_*)_^^_A)_holds_ x_in_A_* let x be set ; ::_thesis: ( x in {(<%> E)} \/ ((A *) ^^ A) implies x in A * ) assume x in {(<%> E)} \/ ((A *) ^^ A) ; ::_thesis: x in A * then ( x in {(<%> E)} or x in (A *) ^^ A ) by XBOOLE_0:def_3; then ( x = <%> E or x in A * ) by Th52, TARSKI:def_1; hence x in A * by Th48; ::_thesis: verum end; A2: now__::_thesis:_for_x_being_set_st_x_in_A_*_holds_ x_in_{(<%>_E)}_\/_((A_*)_^^_A) let x be set ; ::_thesis: ( x in A * implies x in {(<%> E)} \/ ((A *) ^^ A) ) assume x in A * ; ::_thesis: x in {(<%> E)} \/ ((A *) ^^ A) then consider n being Nat such that A3: x in A |^ n by Th41; A4: now__::_thesis:_(_n_>_0_implies_x_in_(A_*)_^^_A_) assume n > 0 ; ::_thesis: x in (A *) ^^ A then ex m being Nat st m + 1 = n by NAT_1:6; hence x in (A *) ^^ A by A3, Th50; ::_thesis: verum end; ( n = 0 implies x in {(<%> E)} ) by A3, Th24; hence x in {(<%> E)} \/ ((A *) ^^ A) by A4, XBOOLE_0:def_3; ::_thesis: verum end; A5: now__::_thesis:_for_x_being_set_st_x_in_A_*_holds_ x_in_{(<%>_E)}_\/_(A_^^_(A_*)) let x be set ; ::_thesis: ( x in A * implies x in {(<%> E)} \/ (A ^^ (A *)) ) assume x in A * ; ::_thesis: x in {(<%> E)} \/ (A ^^ (A *)) then consider n being Nat such that A6: x in A |^ n by Th41; A7: now__::_thesis:_(_n_>_0_implies_x_in_A_^^_(A_*)_) assume n > 0 ; ::_thesis: x in A ^^ (A *) then ex m being Nat st m + 1 = n by NAT_1:6; hence x in A ^^ (A *) by A6, Th50; ::_thesis: verum end; ( n = 0 implies x in {(<%> E)} ) by A6, Th24; hence x in {(<%> E)} \/ (A ^^ (A *)) by A7, XBOOLE_0:def_3; ::_thesis: verum end; now__::_thesis:_for_x_being_set_st_x_in_{(<%>_E)}_\/_(A_^^_(A_*))_holds_ x_in_A_* let x be set ; ::_thesis: ( x in {(<%> E)} \/ (A ^^ (A *)) implies x in A * ) assume x in {(<%> E)} \/ (A ^^ (A *)) ; ::_thesis: x in A * then ( x in {(<%> E)} or x in A ^^ (A *) ) by XBOOLE_0:def_3; then ( x = <%> E or x in A * ) by Th52, TARSKI:def_1; hence x in A * by Th48; ::_thesis: verum end; hence ( A * = {(<%> E)} \/ (A ^^ (A *)) & A * = {(<%> E)} \/ ((A *) ^^ A) ) by A2, A5, A1, TARSKI:1; ::_thesis: verum end; theorem Th57: :: FLANG_1:57 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 * = {(<%> E)} \/ (A ^^ (A *)) & A * = {(<%> E)} \/ ((A *) ^^ A) ) by Th56; now__::_thesis:_A_^^_(A_*)_=_(A_*)_^^_A percases ( <%> E in A or not <%> E in A ) ; supposeA2: <%> E in A ; ::_thesis: A ^^ (A *) = (A *) ^^ A then A * = A ^^ (A *) by Th54; hence A ^^ (A *) = (A *) ^^ A by A2, Th54; ::_thesis: verum end; supposeA3: not <%> E in A ; ::_thesis: A ^^ (A *) = (A *) ^^ A then not <%> E in (A *) ^^ A by Th15; then A4: {(<%> E)} misses (A *) ^^ A by ZFMISC_1:50; not <%> E in A ^^ (A *) by A3, Th15; then {(<%> E)} misses A ^^ (A *) by ZFMISC_1:50; hence A ^^ (A *) = (A *) ^^ A by A1, A4, XBOOLE_1:71; ::_thesis: verum end; end; end; hence A ^^ (A *) = (A *) ^^ A ; ::_thesis: verum end; theorem :: FLANG_1:58 for E being set for A being Subset of (E ^omega) for n being Nat holds (A |^ n) ^^ (A *) = (A *) ^^ (A |^ n) proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for n being Nat holds (A |^ n) ^^ (A *) = (A *) ^^ (A |^ n) let A be Subset of (E ^omega); ::_thesis: for n being Nat holds (A |^ n) ^^ (A *) = (A *) ^^ (A |^ n) let n be Nat; ::_thesis: (A |^ n) ^^ (A *) = (A *) ^^ (A |^ n) defpred S1[ Nat] means (A |^ $1) ^^ (A *) = (A *) ^^ (A |^ $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 |^ (n + 1)) ^^ (A *) = ((A |^ n) ^^ A) ^^ (A *) by Th23 .= (A |^ n) ^^ (A ^^ (A *)) by Th18 .= (A |^ n) ^^ ((A *) ^^ A) by Th57 .= ((A *) ^^ (A |^ n)) ^^ A by A2, Th18 .= (A *) ^^ ((A |^ n) ^^ A) by Th18 .= (A *) ^^ (A |^ (n + 1)) by Th23 ; hence S1[n + 1] ; ::_thesis: verum end; (A |^ 0) ^^ (A *) = {(<%> E)} ^^ (A *) by Th24 .= A * by Th13 .= (A *) ^^ {(<%> E)} by Th13 .= (A *) ^^ (A |^ 0) by Th24 ; then A3: S1[ 0 ] ; for n being Nat holds S1[n] from NAT_1:sch_2(A3, A1); hence (A |^ n) ^^ (A *) = (A *) ^^ (A |^ n) ; ::_thesis: verum end; theorem Th59: :: FLANG_1:59 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 * ) defpred S1[ Nat] means A |^ $1 c= B * ; assume A1: A c= B * ; ::_thesis: A |^ n c= B * A2: 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 S1[n] ; ::_thesis: S1[n + 1] then (A |^ n) ^^ A c= B * by A1, Th46; hence S1[n + 1] by Th23; ::_thesis: verum end; <%> E in B * by Th48; then {(<%> E)} c= B * by ZFMISC_1:31; then A3: S1[ 0 ] by Th24; for n being Nat holds S1[n] from NAT_1:sch_2(A3, A2); hence A |^ n c= B * ; ::_thesis: verum end; theorem Th60: :: FLANG_1:60 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 A1: A c= B * ; ::_thesis: A * c= B * thus A * c= B * ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A * or x in B * ) assume x in A * ; ::_thesis: x in B * then consider n being Nat such that A2: x in A |^ n by Th41; A |^ n c= B * by A1, Th59; hence x in B * by A2; ::_thesis: verum end; end; theorem Th61: :: FLANG_1: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 A1: A c= B ; ::_thesis: A * c= B * B c= B * by Th43; then A c= B * by A1, XBOOLE_1:1; hence A * c= B * by Th60; ::_thesis: verum end; theorem Th62: :: FLANG_1: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 * ( (A *) * c= A * & A * c= (A *) * ) by Th43, Th60; hence (A *) * = A * by XBOOLE_0:def_10; ::_thesis: verum end; theorem :: FLANG_1:63 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 * <%> E in A * by Th48; then A1: A * c= (A *) ^^ (A *) by Th16; (A *) ^^ (A *) c= A * by Th46; hence (A *) ^^ (A *) = A * by A1, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: FLANG_1:64 for E being set for A being Subset of (E ^omega) for n being Nat holds (A |^ n) * c= A * by Th42, Th60; theorem Th65: :: FLANG_1:65 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 * (A *) |^ n c= (A *) * by Th42; hence (A *) |^ n c= A * by Th62; ::_thesis: verum end; theorem :: FLANG_1:66 for E being set for A being Subset of (E ^omega) for n being Nat st n > 0 holds (A *) |^ n = A * proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for n being Nat st n > 0 holds (A *) |^ n = A * let A be Subset of (E ^omega); ::_thesis: for n being Nat st n > 0 holds (A *) |^ n = A * let n be Nat; ::_thesis: ( n > 0 implies (A *) |^ n = A * ) <%> E in A * by Th48; then A1: ( n > 0 implies A * c= (A *) |^ n ) by Th35; (A *) |^ n c= A * by Th65; hence ( n > 0 implies (A *) |^ n = A * ) by A1, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th67: :: FLANG_1:67 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) * ) defpred S1[ Nat] means (B \/ A) |^ $1 c= B * ; assume A1: A c= B * ; ::_thesis: B * = (B \/ A) * A2: 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 A3: S1[n] ; ::_thesis: S1[n + 1] B c= B * by Th43; then A4: B \/ A c= B * by A1, XBOOLE_1:8; (B \/ A) |^ (n + 1) = ((B \/ A) |^ n) ^^ (B \/ A) by Th23; hence S1[n + 1] by A3, A4, Th46; ::_thesis: verum end; ( (B \/ A) |^ 0 = {(<%> E)} & <%> E in B * ) by Th24, Th48; then A5: S1[ 0 ] by ZFMISC_1:31; A6: for n being Nat holds S1[n] from NAT_1:sch_2(A5, A2); A7: (B \/ A) * c= B * proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (B \/ A) * or x in B * ) assume x in (B \/ A) * ; ::_thesis: x in B * then consider n being Nat such that A8: x in (B \/ A) |^ n by Th41; (B \/ A) |^ n c= B * by A6; hence x in B * by A8; ::_thesis: verum end; B * c= (B \/ A) * by Th61, XBOOLE_1:7; hence B * = (B \/ A) * by A7, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th68: :: FLANG_1:68 for E being set for A being Subset of (E ^omega) for a being Element of E ^omega st a in A * holds A * = (A \/ {a}) * proof let E be set ; ::_thesis: for A being Subset of (E ^omega) for a being Element of E ^omega st a in A * holds A * = (A \/ {a}) * let A be Subset of (E ^omega); ::_thesis: for a being Element of E ^omega st a in A * holds A * = (A \/ {a}) * let a be Element of E ^omega ; ::_thesis: ( a in A * implies A * = (A \/ {a}) * ) assume a in A * ; ::_thesis: A * = (A \/ {a}) * then {a} c= A * by ZFMISC_1:31; hence A * = (A \/ {a}) * by Th67; ::_thesis: verum end; theorem :: FLANG_1:69 for E being set for A being Subset of (E ^omega) holds A * = (A \ {(<%> E)}) * proof let E be set ; ::_thesis: for A being Subset of (E ^omega) holds A * = (A \ {(<%> E)}) * let A be Subset of (E ^omega); ::_thesis: A * = (A \ {(<%> E)}) * thus (A \ {(<%> E)}) * = ((A \ {(<%> E)}) \/ {(<%> E)}) * by Th48, Th68 .= (A \/ {(<%> E)}) * by XBOOLE_1:39 .= A * by Th48, Th68 ; ::_thesis: verum end; theorem :: FLANG_1:70 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) * ( A * c= (A \/ B) * & B * c= (A \/ B) * ) by Th61, XBOOLE_1:7; hence (A *) \/ (B *) c= (A \/ B) * by XBOOLE_1:8; ::_thesis: verum end; theorem :: FLANG_1:71 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 *) ( (A /\ B) * c= A * & (A /\ B) * c= B * ) by Th61, XBOOLE_1:17; hence (A /\ B) * c= (A *) /\ (B *) by XBOOLE_1:19; ::_thesis: verum end; theorem Th72: :: FLANG_1:72 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 ) thus ( <%x%> in A * implies <%x%> in A ) ::_thesis: ( <%x%> in A implies <%x%> in A * ) proof defpred S1[ Nat] means <%x%> in A |^ $1; assume that A1: <%x%> in A * and A2: not <%x%> in A ; ::_thesis: contradiction A3: ex i being Nat st S1[i] by A1, Th41; ex n1 being Nat st ( S1[n1] & ( for n2 being Nat st S1[n2] holds n1 <= n2 ) ) from NAT_1:sch_5(A3); then consider n1 being Nat such that A4: S1[n1] and A5: for n2 being Nat st S1[n2] holds n1 <= n2 ; A6: now__::_thesis:_not_n1_=_0 assume n1 = 0 ; ::_thesis: contradiction then <%x%> in {(<%> E)} by A4, Th24; hence contradiction by TARSKI:def_1; ::_thesis: verum end; A7: now__::_thesis:_(_n1_>_1_implies_<%x%>_in_A_) assume n1 > 1 ; ::_thesis: <%x%> in A then consider n2 being Nat such that A8: n2 + 1 = n1 by NAT_1:6; <%x%> in (A |^ n2) ^^ A by A4, A8, Th23; then consider a, b being Element of E ^omega such that A9: a in A |^ n2 and A10: ( b in A & <%x%> = a ^ b ) by Def1; now__::_thesis:_(_a_=_<%x%>_implies_not_b_=_<%>_E_) reconsider n2 = n2 as Element of NAT by ORDINAL1:def_12; assume that A11: a = <%x%> and b = <%> E ; ::_thesis: contradiction ex i being Element of NAT st ( S1[i] & n1 > i ) proof take n2 ; ::_thesis: ( S1[n2] & n1 > n2 ) thus ( S1[n2] & n1 > n2 ) by A8, A9, A11, NAT_1:13; ::_thesis: verum end; hence contradiction by A5; ::_thesis: verum end; hence <%x%> in A by A10, Th4; ::_thesis: verum end; ( n1 = 1 implies <%x%> in A ) by A4, Th25; hence contradiction by A2, A7, A6, NAT_1:25; ::_thesis: verum end; assume <%x%> in A ; ::_thesis: <%x%> in A * then <%x%> in A |^ 1 by Th25; hence <%x%> in A * by Th41; ::_thesis: verum end; begin definition let E be set ; func Lex E -> Subset of (E ^omega) means :Def4: :: FLANG_1:def 4 for x being set holds ( x in it iff ex e being Element of E st ( e in E & x = <%e%> ) ); existence ex b1 being Subset of (E ^omega) st for x being set holds ( x in b1 iff ex e being Element of E st ( e in E & x = <%e%> ) ) proof defpred S1[ set ] means ex e being Element of E st ( e in E & $1 = <%e%> ); consider C being Subset of (E ^omega) such that A1: for x being set holds ( x in C iff ( x in E ^omega & S1[x] ) ) from SUBSET_1:sch_1(); take C ; ::_thesis: for x being set holds ( x in C iff ex e being Element of E st ( e in E & x = <%e%> ) ) for x being set holds ( x in C iff ex e being Element of E st ( e in E & x = <%e%> ) ) proof let x be set ; ::_thesis: ( x in C iff ex e being Element of E st ( e in E & x = <%e%> ) ) thus ( x in C implies ex e being Element of E st ( e in E & x = <%e%> ) ) by A1; ::_thesis: ( ex e being Element of E st ( e in E & x = <%e%> ) implies x in C ) given e being Element of E such that A2: e in E and A3: x = <%e%> ; ::_thesis: x in C {e} c= E by A2, ZFMISC_1:31; then rng <%e%> c= E by AFINSQ_1:33; then <%e%> is XFinSequence of by RELAT_1:def_19; then <%e%> is Element of E ^omega by AFINSQ_1:def_7; hence x in C by A1, A2, A3; ::_thesis: verum end; hence for x being set holds ( x in C iff ex e being Element of E st ( e in E & x = <%e%> ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being Subset of (E ^omega) st ( for x being set holds ( x in b1 iff ex e being Element of E st ( e in E & x = <%e%> ) ) ) & ( for x being set holds ( x in b2 iff ex e being Element of E st ( e in E & x = <%e%> ) ) ) holds b1 = b2 proof let C1, C2 be Subset of (E ^omega); ::_thesis: ( ( for x being set holds ( x in C1 iff ex e being Element of E st ( e in E & x = <%e%> ) ) ) & ( for x being set holds ( x in C2 iff ex e being Element of E st ( e in E & x = <%e%> ) ) ) implies C1 = C2 ) assume that A4: for x being set holds ( x in C1 iff ex e being Element of E st ( e in E & x = <%e%> ) ) and A5: for x being set holds ( x in C2 iff ex e being Element of E st ( e in E & x = <%e%> ) ) ; ::_thesis: C1 = C2 now__::_thesis:_for_x_being_set_holds_ (_(_x_in_C1_implies_x_in_C2_)_&_(_x_in_C2_implies_x_in_C1_)_) let x be set ; ::_thesis: ( ( x in C1 implies x in C2 ) & ( x in C2 implies x in C1 ) ) thus ( x in C1 implies x in C2 ) ::_thesis: ( x in C2 implies x in C1 ) proof assume x in C1 ; ::_thesis: x in C2 then ex e being Element of E st ( e in E & x = <%e%> ) by A4; hence x in C2 by A5; ::_thesis: verum end; assume x in C2 ; ::_thesis: x in C1 then ex e being Element of E st ( e in E & x = <%e%> ) by A5; hence x in C1 by A4; ::_thesis: verum end; hence C1 = C2 by TARSKI:1; ::_thesis: verum end; end; :: deftheorem Def4 defines Lex FLANG_1:def_4_:_ for E being set for b2 being Subset of (E ^omega) holds ( b2 = Lex E iff for x being set holds ( x in b2 iff ex e being Element of E st ( e in E & x = <%e%> ) ) ); theorem Th73: :: FLANG_1:73 for E being set for a being Element of E ^omega holds a in (Lex E) |^ (len a) proof let E be set ; ::_thesis: for a being Element of E ^omega holds a in (Lex E) |^ (len a) let a be Element of E ^omega ; ::_thesis: a in (Lex E) |^ (len a) defpred S1[ Nat] means for a being Element of E ^omega st len a = $1 holds a in (Lex E) |^ $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:_for_b_being_Element_of_E_^omega_st_len_b_=_n_+_1_holds_ b_in_(Lex_E)_|^_(n_+_1) let b be Element of E ^omega ; ::_thesis: ( len b = n + 1 implies b in (Lex E) |^ (n + 1) ) assume len b = n + 1 ; ::_thesis: b in (Lex E) |^ (n + 1) then consider c being Element of E ^omega , e being Element of E such that A3: len c = n and A4: b = c ^ <%e%> by Th7; <%e%> is Element of E ^omega by A4, Th5; then e in E by Th6; then <%e%> in Lex E by Def4; then A5: <%e%> in (Lex E) |^ 1 by Th25; c in (Lex E) |^ n by A2, A3; hence b in (Lex E) |^ (n + 1) by A4, A5, Th40; ::_thesis: verum end; hence S1[n + 1] ; ::_thesis: verum end; A6: S1[ 0 ] proof let a be Element of E ^omega ; ::_thesis: ( len a = 0 implies a in (Lex E) |^ 0 ) assume len a = 0 ; ::_thesis: a in (Lex E) |^ 0 then a = <%> E ; then a in {(<%> E)} by TARSKI:def_1; hence a in (Lex E) |^ 0 by Th24; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A6, A1); hence a in (Lex E) |^ (len a) ; ::_thesis: verum end; theorem :: FLANG_1:74 for E being set holds (Lex E) * = E ^omega proof let E be set ; ::_thesis: (Lex E) * = E ^omega A1: now__::_thesis:_for_x_being_set_st_x_in_E_^omega_holds_ x_in_(Lex_E)_* let x be set ; ::_thesis: ( x in E ^omega implies x in (Lex E) * ) assume x in E ^omega ; ::_thesis: x in (Lex E) * then reconsider a = x as Element of E ^omega ; a in (Lex E) |^ (len a) by Th73; hence x in (Lex E) * by Th41; ::_thesis: verum end; for x being set st x in (Lex E) * holds x in E ^omega ; hence (Lex E) * = E ^omega by A1, TARSKI:1; ::_thesis: verum end; theorem :: FLANG_1:75 for E being set for A being Subset of (E ^omega) st A * = E ^omega holds Lex E c= A proof let E be set ; ::_thesis: for A being Subset of (E ^omega) st A * = E ^omega holds Lex E c= A let A be Subset of (E ^omega); ::_thesis: ( A * = E ^omega implies Lex E c= A ) assume A1: A * = E ^omega ; ::_thesis: Lex E c= A thus Lex E c= A ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Lex E or x in A ) assume A2: x in Lex E ; ::_thesis: x in A then ex e being Element of E st ( e in E & x = <%e%> ) by Def4; hence x in A by A1, A2, Th72; ::_thesis: verum end; end;