flang_1.miz

    begin

    reserve E,x,y,X for set;

    reserve A,B,C,D for Subset of (E ^omega );

    reserve a,a1,a2,b,c,c1,c2,d,ab,bc for Element of (E ^omega );

    reserve e for Element of E;

    reserve i,j,k,l,n,n1,n2,m for Nat;

    definition

      let E, a, b;

      :: original: ^

      redefine

      func a ^ b -> Element of (E ^omega ) ;

      coherence by AFINSQ_1:def 7;

    end

    definition

      let E;

      :: original: <%>

      redefine

      func <%> E -> Element of (E ^omega ) ;

      coherence 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 by AFINSQ_1:def 7;

    end

    definition

      let E, a;

      :: original: {

      redefine

      func {a} -> Subset of (E ^omega ) ;

      coherence by SUBSET_1: 33;

    end

    definition

      let E;

      let f be sequence of ( bool E);

      let n;

      :: original: .

      redefine

      func f . n -> Subset of E ;

      coherence

      proof

        n is Element of NAT by ORDINAL1:def 12;

        then (f . n) in ( rng f) by FUNCT_2: 112;

        hence thesis;

      end;

    end

    theorem :: FLANG_1:1



     Th1: n1 > n or n2 > n implies (n1 + n2) > n

    proof



       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;

      hence thesis by A1, A2;

    end;

    theorem :: FLANG_1:2



     Th2: (n1 + n) <= (n2 + 1) & n > 0 implies n1 <= n2

    proof

      assume that

       A1: (n1 + n) <= (n2 + 1) and

       A2: n > 0 ;

      (1 + 0 ) <= n by A2, NAT_1: 13;

      hence thesis by A1, XREAL_1: 8;

    end;

    theorem :: FLANG_1:3



     Th3: (n1 + n2) = 1 iff n1 = 1 & n2 = 0 or n1 = 0 & n2 = 1

    proof

      thus (n1 + n2) = 1 implies n1 = 1 & n2 = 0 or n1 = 0 & n2 = 1

      proof

        assume

         A1: (n1 + n2) = 1;

        now



           A2: n1 = 0 & n2 = 0 implies contradiction by A1;

          assume

           A3: n1 <= 1 & n2 <= 1;

          n1 = 1 & n2 = 1 implies contradiction by A1;

          hence thesis by A3, A2, NAT_1: 25;

        end;

        hence thesis by A1, Th1;

      end;

      thus thesis;

    end;

    theorem :: FLANG_1:4



     Th4: (a ^ b) = <%x%> iff a = ( <%> E) & b = <%x%> or b = ( <%> E) & a = <%x%>

    proof

      thus (a ^ b) = <%x%> implies a = ( <%> E) & b = <%x%> or b = ( <%> E) & a = <%x%>

      proof

        assume

         A1: (a ^ b) = <%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 thesis by A1;

      end;

      assume a = ( <%> E) & b = <%x%> or b = ( <%> E) & a = <%x%>;

      hence thesis;

    end;

    theorem :: FLANG_1:5



     Th5: for p,q be XFinSequence holds a = (p ^ q) implies p is Element of (E ^omega ) & q is Element of (E ^omega )

    proof

      let p,q be XFinSequence;

      assume a = (p ^ q);

      then p is XFinSequence of E & q is XFinSequence of E by AFINSQ_1: 31;

      hence thesis by AFINSQ_1:def 7;

    end;

    theorem :: FLANG_1:6



     Th6: for x be object holds <%x%> is Element of (E ^omega ) implies x in E

    proof

      let x be object;

      assume <%x%> is Element of (E ^omega );

      then ( rng <%x%>) c= E by RELAT_1:def 19;

      then {x} c= E by AFINSQ_1: 33;

      hence thesis by ZFMISC_1: 31;

    end;

    theorem :: FLANG_1:7



     Th7: ( len b) = (n + 1) implies ex c, e st ( len c) = n & b = (c ^ <%e%>)

    proof

      assume

       A1: ( len b) = (n + 1);

      then b <> {} ;

      then

      consider c9 be XFinSequence, x be object 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, e;

      (n + 1) = (( len c) + ( len <%x%>)) by A1, A2, AFINSQ_1: 17

      .= (( len c) + 1) by AFINSQ_1: 34;

      hence thesis by A2;

    end;

    theorem :: FLANG_1:8



     Th8: for p be XFinSequence st p <> {} holds ex q be XFinSequence, x be object st p = ( <%x%> ^ q)

    proof

      let p be XFinSequence;

      defpred P[ Nat] means for p be XFinSequence st ( len p) = $1 & p <> {} holds ex q be XFinSequence, x be object st p = ( <%x%> ^ q);

       A1:

      now

        let n;

        assume

         A2: P[n];

        thus P[(n + 1)]

        proof

          let p be XFinSequence such that

           A3: ( len p) = (n + 1) and

           A4: p <> {} ;

          consider q be XFinSequence, x be object 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: 34;

          per cases ;

            suppose q = {} ;



            then p = ( {} ^ <%x%>) by A5

            .= ( <%x%> ^ {} );

            hence thesis;

          end;

            suppose q <> {} ;

            then

            consider r be XFinSequence, y be object such that

             A7: q = ( <%y%> ^ r) by A2, A6;

            p = ( <%y%> ^ (r ^ <%x%>)) by A5, A7, AFINSQ_1: 27;

            hence thesis;

          end;

        end;

      end;



       A8: P[ 0 ];



       A9: for n holds P[n] from NAT_1:sch 2( A8, A1);



       A10: ( len p) = ( len p);

      assume p <> {} ;

      hence thesis by A9, A10;

    end;

    theorem :: FLANG_1:9

    ( len b) = (n + 1) implies ex c, e st ( len c) = n & b = ( <%e%> ^ c)

    proof

      assume

       A1: ( len b) = (n + 1);

      then b <> {} ;

      then

      consider c9 be XFinSequence, x be object 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, e;

      (n + 1) = (( len c) + ( len <%x%>)) by A1, A2, AFINSQ_1: 17

      .= (( len c) + 1) by AFINSQ_1: 34;

      hence thesis by A2;

    end;



     Lm1: for p be XFinSequence st ( len p) = (i + j) holds ex q1,q2 be XFinSequence st ( len q1) = i & ( len q2) = j & p = (q1 ^ q2) by AFINSQ_1: 61;

    theorem :: FLANG_1:10

    ( len b) = (n + m) implies ex c1, c2 st ( len c1) = n & ( len c2) = m & b = (c1 ^ c2)

    proof

      assume ( len b) = (n + m);

      then

      consider c19,c29 be 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, c2;

      thus thesis by A1, A2;

    end;

    theorem :: FLANG_1:11



     Th11: (a ^ a) = a implies a = {}

    proof

      assume (a ^ a) = a;

      then (( len a) + ( len a)) = ( len a) by AFINSQ_1: 17;

      hence thesis;

    end;

    begin

    definition

      let E, A, B;

      :: FLANG_1:def1

      func A ^^ B -> Subset of (E ^omega ) means

      : Def1: x in it iff ex a, b st a in A & b in B & x = (a ^ b);

      existence

      proof

        defpred P[ set] means ex a, b st a in A & b in B & $1 = (a ^ b);

        consider C such that

         A1: x in C iff x in (E ^omega ) & P[x] from SUBSET_1:sch 1;

        take C;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let C1,C2 be Subset of (E ^omega ) such that

         A2: x in C1 iff ex a, b st a in A & b in B & x = (a ^ b) and

         A3: x in C2 iff ex a, b st a in A & b in B & x = (a ^ b);

        now

          let x be object;

          thus x in C1 implies x in C2

          proof

            assume x in C1;

            then ex a, b st a in A & b in B & x = (a ^ b) by A2;

            hence thesis by A3;

          end;

          assume x in C2;

          then ex a, b st a in A & b in B & x = (a ^ b) by A3;

          hence x in C1 by A2;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    theorem :: FLANG_1:12



     Th12: (A ^^ B) = {} iff A = {} or B = {}

    proof

      thus (A ^^ B) = {} implies A = {} or B = {}

      proof

        assume that

         A1: (A ^^ B) = {} and

         A2: A <> {} and

         A3: B <> {} ;

        consider a such that

         A4: a in A by A2, SUBSET_1: 4;

        consider b such that

         A5: b in B by A3, SUBSET_1: 4;

        (a ^ b) in (A ^^ B) by A4, A5, Def1;

        hence contradiction by A1;

      end;

      assume

       A6: A = {} or B = {} ;

       not ex x be object st x in (A ^^ B)

      proof

        given x be object such that

         A7: x in (A ^^ B);

        ex a, b st a in A & b in B & x = (a ^ b) by A7, Def1;

        hence contradiction by A6;

      end;

      hence thesis by XBOOLE_0:def 1;

    end;

    theorem :: FLANG_1:13



     Th13: (A ^^ {( <%> E)}) = A & ( {( <%> E)} ^^ A) = A

    proof



       A1: for x be object holds x in (A ^^ {( <%> E)}) implies x in A

      proof

        let x be object;

        assume x in (A ^^ {( <%> E)});

        then

        consider a, d such that

         A2: a in A and

         A3: d in {( <%> E)} & x = (a ^ d) by Def1;

        x = (a ^ {} ) by A3, TARSKI:def 1;

        hence thesis by A2;

      end;



       A4: for x be object holds x in A implies x in ( {( <%> E)} ^^ A)

      proof

        let x be object;

        assume

         A5: x in A;

        ex d, a st d in {( <%> E)} & a in A & x = (d ^ a)

        proof

          reconsider a = x as Element of (E ^omega ) by A5;

          consider d such that

           A6: d = ( <%> E);

          take d, a;

          thus thesis by A5, A6, TARSKI:def 1;

        end;

        hence thesis by Def1;

      end;



       A7: for x be object holds x in A implies x in (A ^^ {( <%> E)})

      proof

        let x be object;

        assume

         A8: x in A;

        ex a, d 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, d;

          thus thesis by A8, TARSKI:def 1;

        end;

        hence thesis by Def1;

      end;

      for x be object holds x in ( {( <%> E)} ^^ A) implies x in A

      proof

        let x be object;

        assume x in ( {( <%> E)} ^^ A);

        then

        consider d, a 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 thesis by A10;

      end;

      hence thesis by A1, A4, A7, TARSKI: 2;

    end;

    theorem :: FLANG_1:14



     Th14: (A ^^ B) = {( <%> E)} iff A = {( <%> E)} & B = {( <%> E)}

    proof

      thus (A ^^ B) = {( <%> E)} implies A = {( <%> E)} & B = {( <%> E)}

      proof

        assume that

         A1: (A ^^ B) = {( <%> E)} and

         A2: A <> {( <%> E)} or B <> {( <%> E)};

        ( <%> E) in (A ^^ B) by A1, TARSKI:def 1;

        then

        consider a, b such that

         A3: a in A and

         A4: b in B and ( <%> E) = (a ^ b) by Def1;

         A5:

        now

          let x;

          assume that

           A6: x in A or x in B and

           A7: x <> ( <%> E);

           A8:

          now

            assume

             A9: x in B;

            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;

          end;

          now

            assume

             A11: x in A;

            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;

          end;

          hence contradiction by A6, A8;

        end;

        then

         A13: for x be object holds x in B iff x = ( <%> E) by A4;

        for x be object holds x in A iff x = ( <%> E) by A3, A5;

        hence contradiction by A2, A13, TARSKI:def 1;

      end;

      assume A = {( <%> E)} & B = {( <%> E)};

      hence thesis by Th13;

    end;

    theorem :: FLANG_1:15



     Th15: ( <%> E) in (A ^^ B) iff ( <%> E) in A & ( <%> E) in B

    proof

      thus ( <%> E) in (A ^^ B) implies ( <%> E) in A & ( <%> E) in B

      proof

        assume ( <%> E) in (A ^^ B);

        then ex a, b st a in A & b in B & (a ^ b) = ( <%> E) by Def1;

        hence thesis by AFINSQ_1: 30;

      end;

      assume ( <%> E) in A & ( <%> E) in B;

      then ( {} ^ ( <%> E)) in (A ^^ B) by Def1;

      hence thesis;

    end;

    theorem :: FLANG_1:16



     Th16: ( <%> E) in B implies A c= (A ^^ B) & A c= (B ^^ A)

    proof

      assume

       A1: ( <%> E) in B;

      thus A c= (A ^^ B)

      proof

        let x be object;

        assume

         A2: x in A;

        then

        reconsider xa = x as Element of (E ^omega );

        (xa ^ {} ) in (A ^^ B) by A1, A2, Def1;

        hence thesis;

      end;

      thus A c= (B ^^ A)

      proof

        let x be object;

        assume

         A3: x in A;

        then

        reconsider xa = x as Element of (E ^omega );

        ( {} ^ xa) in (B ^^ A) by A1, A3, Def1;

        hence thesis;

      end;

    end;

    theorem :: FLANG_1:17



     Th17: A c= C & B c= D implies (A ^^ B) c= (C ^^ D)

    proof

      assume

       A1: A c= C & B c= D;

      thus thesis

      proof

        let x be object;

        assume x in (A ^^ B);

        then ex a, b st a in A & b in B & x = (a ^ b) by Def1;

        hence thesis by A1, Def1;

      end;

    end;

    theorem :: FLANG_1:18



     Th18: ((A ^^ B) ^^ C) = (A ^^ (B ^^ C))

    proof

      now

        let x be object;

        thus x in ((A ^^ B) ^^ C) implies x in (A ^^ (B ^^ C))

        proof

          assume x in ((A ^^ B) ^^ C);

          then

          consider ab, c such that

           A1: ab in (A ^^ B) and

           A2: c in C & x = (ab ^ c) by Def1;

          consider a, b 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 thesis by A3, Def1;

        end;

        assume x in (A ^^ (B ^^ C));

        then

        consider a, bc such that

         A5: a in A and

         A6: bc in (B ^^ C) and

         A7: x = (a ^ bc) by Def1;

        consider b, c 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;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: FLANG_1:19



     Th19: (A ^^ (B /\ C)) c= ((A ^^ B) /\ (A ^^ C)) & ((B /\ C) ^^ A) c= ((B ^^ A) /\ (C ^^ A))

    proof

      thus (A ^^ (B /\ C)) c= ((A ^^ B) /\ (A ^^ C))

      proof

        let x be object;

        assume x in (A ^^ (B /\ C));

        then

        consider a, bc 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 thesis by A4, XBOOLE_0:def 4;

      end;

      thus ((B /\ C) ^^ A) c= ((B ^^ A) /\ (C ^^ A))

      proof

        let x be object;

        assume x in ((B /\ C) ^^ A);

        then

        consider bc, a 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 thesis by A7, XBOOLE_0:def 4;

      end;

    end;

    theorem :: FLANG_1:20



     Th20: ((A ^^ B) \/ (A ^^ C)) = (A ^^ (B \/ C)) & ((B ^^ A) \/ (C ^^ A)) = ((B \/ C) ^^ A)

    proof



       A1: (A ^^ (B \/ C)) c= ((A ^^ B) \/ (A ^^ C))

      proof

        let x be object;

        assume x in (A ^^ (B \/ C));

        then

        consider a, bc 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 thesis by XBOOLE_0:def 3;

      end;



       A5: ((B \/ C) ^^ A) c= ((B ^^ A) \/ (C ^^ A))

      proof

        let x be object;

        assume x in ((B \/ C) ^^ A);

        then

        consider bc, a 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 thesis by XBOOLE_0:def 3;

      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 thesis by A1, A5, A9, XBOOLE_0:def 10;

    end;

    theorem :: FLANG_1:21



     Th21: ((A ^^ B) \ (A ^^ C)) c= (A ^^ (B \ C)) & ((B ^^ A) \ (C ^^ A)) c= ((B \ C) ^^ A)

    proof

      thus ((A ^^ B) \ (A ^^ C)) c= (A ^^ (B \ C))

      proof

        let x be object;

        assume

         A1: x in ((A ^^ B) \ (A ^^ C));

        then x in (A ^^ B) by XBOOLE_0:def 5;

        then

        consider a, b such that

         A2: a in A and

         A3: b in B and

         A4: x = (a ^ b) by Def1;

         A5:

        now

          assume not b in C;

          then b in (B \ C) by A3, XBOOLE_0:def 5;

          hence thesis by A2, A4, Def1;

        end;

         not x in (A ^^ C) by A1, XBOOLE_0:def 5;

        hence thesis by A2, A4, A5, Def1;

      end;

      thus ((B ^^ A) \ (C ^^ A)) c= ((B \ C) ^^ A)

      proof

        let x be object;

        assume

         A6: x in ((B ^^ A) \ (C ^^ A));

        then x in (B ^^ A) by XBOOLE_0:def 5;

        then

        consider b, a such that

         A7: b in B and

         A8: a in A & x = (b ^ a) by Def1;

         A9:

        now

          assume not b in C;

          then b in (B \ C) by A7, XBOOLE_0:def 5;

          hence thesis by A8, Def1;

        end;

         not x in (C ^^ A) by A6, XBOOLE_0:def 5;

        hence thesis by A8, A9, Def1;

      end;

    end;

    theorem :: FLANG_1:22

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

    proof

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

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

      hence thesis by A3, XBOOLE_1: 101;

    end;

    begin

    definition

      let E, A, n;

      :: FLANG_1:def2

      func A |^ n -> Subset of (E ^omega ) means

      : Def2: ex concat be sequence of ( bool (E ^omega )) st it = (concat . n) & (concat . 0 ) = {( <%> E)} & for i holds (concat . (i + 1)) = ((concat . i) ^^ A);

      existence

      proof

        defpred P[ set, set, set] means ex B, C st C = $3 & B = $2 & C = (B ^^ A);



         A1: for i be Nat holds for x be Element of ( bool (E ^omega )) holds ex y be Element of ( bool (E ^omega )) st P[i, x, y]

        proof

          let i be Nat;

          let x be Element of ( bool (E ^omega ));

          take (x ^^ A);

          thus thesis;

        end;

        consider f be sequence of ( bool (E ^omega )) such that

         A2: (f . 0 ) = {( <%> E)} & for i be Nat holds P[i, (f . i), (f . (i + 1))] from RECDEF_1:sch 2( A1);

        consider C be Subset of (E ^omega ) such that

         A3: C = (f . n);

        take C;

        now

          let i;

          reconsider j = i as Element of NAT by ORDINAL1:def 12;

          ex B, C st C = (f . (j + 1)) & B = (f . j) & C = (B ^^ A) by A2;

          hence (f . (i + 1)) = ((f . i) ^^ A);

        end;

        hence thesis by A2, A3;

      end;

      uniqueness

      proof

        let C1,C2 be Subset of (E ^omega );

        given f1 be sequence of ( bool (E ^omega )) such that

         A4: C1 = (f1 . n) and

         A5: (f1 . 0 ) = {( <%> E)} and

         A6: for i holds (f1 . (i + 1)) = ((f1 . i) ^^ A);

        given f2 be sequence of ( bool (E ^omega )) such that

         A7: C2 = (f2 . n) and

         A8: (f2 . 0 ) = {( <%> E)} and

         A9: for i holds (f2 . (i + 1)) = ((f2 . i) ^^ A);

        defpred P[ Nat] means (f1 . $1) = (f2 . $1);

         A10:

        now

          let k;

          assume

           A11: P[k];

          (f2 . (k + 1)) = ((f2 . k) ^^ A) by A9;

          hence P[(k + 1)] by A6, A11;

        end;



         A12: P[ 0 ] by A5, A8;

        for k holds P[k] from NAT_1:sch 2( A12, A10);

        hence thesis by A4, A7;

      end;

    end

    theorem :: FLANG_1:23



     Th23: (A |^ (n + 1)) = ((A |^ n) ^^ A)

    proof

      consider concat be sequence of ( bool (E ^omega )) such that

       A1: (A |^ n) = (concat . n) and

       A2: (concat . 0 ) = {( <%> E)} and

       A3: for i holds (concat . (i + 1)) = ((concat . i) ^^ A) by Def2;

      (concat . (n + 1)) = ((A |^ n) ^^ A) by A1, A3;

      hence thesis by A2, A3, Def2;

    end;

    theorem :: FLANG_1:24



     Th24: (A |^ 0 ) = {( <%> E)}

    proof

      ex concat be sequence of ( bool (E ^omega )) st (A |^ 0 ) = (concat . 0 ) & (concat . 0 ) = {( <%> E)} & for i holds (concat . (i + 1)) = ((concat . i) ^^ A) by Def2;

      hence thesis;

    end;

    theorem :: FLANG_1:25



     Th25: (A |^ 1) = A

    proof

      consider concat be sequence of ( bool (E ^omega )) such that

       A1: (A |^ 1) = (concat . 1) and

       A2: (concat . 0 ) = {( <%> E)} & for i holds (concat . (i + 1)) = ((concat . i) ^^ A) by Def2;



      thus (A |^ 1) = (concat . ( 0 + 1)) by A1

      .= ( {( <%> E)} ^^ A) by A2

      .= A by Th13;

    end;

    theorem :: FLANG_1:26



     Th26: (A |^ 2) = (A ^^ A)

    proof



      thus (A |^ 2) = (A |^ (1 + 1))

      .= ((A |^ 1) ^^ A) by Th23

      .= (A ^^ A) by Th25;

    end;

    theorem :: FLANG_1:27



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

    proof

      defpred P[ Nat] means (A |^ $1) = {} ;

      thus (A |^ n) = {} implies n > 0 & A = {}

      proof

        assume that

         A1: (A |^ n) = {} and

         A2: n <= 0 or A <> {} ;

         A3:

        now

          defpred P[ Nat] means (A |^ $1) <> {} ;

          assume

           A4: A <> {} ;

           A5:

          now

            let n;

            assume P[n];

            then

            consider a1 such that

             A6: a1 in (A |^ n) by SUBSET_1: 4;

            consider a2 such that

             A7: a2 in A by A4, SUBSET_1: 4;

            (a1 ^ a2) in ((A |^ n) ^^ A) by A6, A7, Def1;

            hence P[(n + 1)] by Th23;

          end;

          (A |^ 0 ) = {( <%> E)} by Th24;

          then

           A8: P[ 0 ];

          for n holds P[n] from NAT_1:sch 2( A8, A5);

          hence contradiction by A1;

        end;

        now

          assume n <= 0 ;

          then n = 0 ;

          then (A |^ n) = {( <%> E)} by Th24;

          hence contradiction by A1;

        end;

        hence thesis by A2, A3;

      end;

      assume that

       A9: n > 0 and

       A10: A = {} ;

       A11:

      now

        let m be Nat;

        assume that 1 <= m and P[m];

        (( {} (E ^omega )) |^ (m + 1)) = ((( {} (E ^omega )) |^ m) ^^ ( {} (E ^omega ))) by Th23

        .= {} by Th12;

        hence P[(m + 1)] by A10;

      end;



       A12: P[1] by A10, Th25;



       A13: for m be Nat st m >= 1 holds P[m] from NAT_1:sch 8( A12, A11);

      n >= ( 0 + 1) by A9, NAT_1: 13;

      hence thesis by A13;

    end;

    theorem :: FLANG_1:28



     Th28: ( {( <%> E)} |^ n) = {( <%> E)}

    proof

      defpred P[ Nat] means ( {( <%> E)} |^ $1) = {( <%> E)};

       A1:

      now

        let n;

        assume

         A2: P[n];

        ( {( <%> E)} |^ (n + 1)) = (( {( <%> E)} |^ n) ^^ {( <%> E)}) by Th23

        .= {( <%> E)} by A2, Th13;

        hence P[(n + 1)];

      end;



       A3: P[ 0 ] by Th24;

      for n holds P[n] from NAT_1:sch 2( A3, A1);

      hence thesis;

    end;

    theorem :: FLANG_1:29

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

    proof

      thus (A |^ n) = {( <%> E)} implies n = 0 or A = {( <%> E)}

      proof

        assume

         A1: (A |^ n) = {( <%> E)};

        now

          assume n > 0 ;

          then

          consider m such that

           A2: (m + 1) = n by NAT_1: 6;

          (A |^ n) = ((A |^ m) ^^ A) by A2, Th23;

          hence A = {( <%> E)} by A1, Th14;

        end;

        hence thesis;

      end;

      assume n = 0 or A = {( <%> E)};

      hence thesis by Th24, Th28;

    end;

    theorem :: FLANG_1:30



     Th30: ( <%> E) in A implies ( <%> E) in (A |^ n)

    proof

      defpred P[ Nat] means ( <%> E) in (A |^ $1);

      assume

       A1: ( <%> E) in A;

       A2:

      now

        let n;

        assume P[n];

        then ( <%> E) in ((A |^ n) ^^ A) by A1, Th15;

        hence P[(n + 1)] by Th23;

      end;

      (A |^ 0 ) = {( <%> E)} by Th24;

      then

       A3: P[ 0 ] by TARSKI:def 1;

      for n holds P[n] from NAT_1:sch 2( A3, A2);

      hence thesis;

    end;

    theorem :: FLANG_1:31

    ( <%> E) in (A |^ n) & n > 0 implies ( <%> E) in A

    proof

      assume that

       A1: ( <%> E) in (A |^ n) and

       A2: n > 0 ;

      consider m such that

       A3: (m + 1) = n by A2, NAT_1: 6;

      (A |^ n) = ((A |^ m) ^^ A) by A3, Th23;

      then ex a1, a2 st a1 in (A |^ m) & a2 in A & (a1 ^ a2) = ( <%> E) by A1, Def1;

      hence thesis by AFINSQ_1: 30;

    end;

    theorem :: FLANG_1:32



     Th32: ((A |^ n) ^^ A) = (A ^^ (A |^ n))

    proof

      defpred P[ Nat] means ((A |^ $1) ^^ A) = (A ^^ (A |^ $1));

       A1:

      now

        let n;

        assume

         A2: P[n];

        ((A |^ (n + 1)) ^^ A) = (((A |^ n) ^^ A) ^^ A) by Th23

        .= (A ^^ ((A |^ n) ^^ A)) by A2, Th18

        .= (A ^^ (A |^ (n + 1))) by Th23;

        hence P[(n + 1)];

      end;

      ((A |^ 0 ) ^^ A) = ( {( <%> E)} ^^ A) by Th24

      .= A by Th13

      .= (A ^^ {( <%> E)}) by Th13

      .= (A ^^ (A |^ 0 )) by Th24;

      then

       A3: P[ 0 ];

      for n holds P[n] from NAT_1:sch 2( A3, A1);

      hence thesis;

    end;

    theorem :: FLANG_1:33



     Th33: (A |^ (m + n)) = ((A |^ m) ^^ (A |^ n))

    proof

      defpred P[ Nat] means for m, n st (m + n) <= $1 holds (A |^ (m + n)) = ((A |^ m) ^^ (A |^ n));

       A1:

      now

        let l;

        assume

         A2: P[l];

        now

          let m,n be Nat;

           A3:

          now

            assume (m + n) < (l + 1);

            then (m + n) <= l by NAT_1: 13;

            hence (A |^ (m + n)) = ((A |^ m) ^^ (A |^ n)) by A2;

          end;

           A4:

          now

            assume

             A5: (m + n) = (l + 1);

             A6:

            now

              assume

               A7: n = 0 ;



              thus (A |^ (m + n)) = ((A |^ (l + 1)) ^^ {( <%> E)}) by A5, Th13

              .= ((A |^ m) ^^ (A |^ n)) by A5, A7, Th24;

            end;

             A8:

            now

              assume that

               A9: m > 0 and

               A10: n > 0 ;

              consider k 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));

            end;

            now

              assume

               A12: m = 0 ;



              thus (A |^ (m + n)) = ( {( <%> E)} ^^ (A |^ (l + 1))) by A5, Th13

              .= ((A |^ m) ^^ (A |^ n)) by A5, A12, Th24;

            end;

            hence (A |^ (m + n)) = ((A |^ m) ^^ (A |^ n)) by A6, A8;

          end;

          assume (m + n) <= (l + 1);

          hence (A |^ (m + n)) = ((A |^ m) ^^ (A |^ n)) by A4, A3, XXREAL_0: 1;

        end;

        hence P[(l + 1)];

      end;



       A13: P[ 0 ]

      proof

        let m, n;

        assume

         A14: (m + n) <= 0 ;

        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;

      end;

      for l holds P[l] from NAT_1:sch 2( A13, A1);

      hence thesis;

    end;

    theorem :: FLANG_1:34

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

    proof

      defpred P[ Nat] means for m, n st (m + n) <= $1 holds ((A |^ m) |^ n) = (A |^ (m * n));

       A1:

      now

        let l;

        assume

         A2: P[l];

        now

          let m, n;

           A3:

          now

            assume (m + n) < (l + 1);

            then (m + n) <= l by NAT_1: 13;

            hence ((A |^ m) |^ n) = (A |^ (m * n)) by A2;

          end;

           A4:

          now

            assume

             A5: (m + n) = (l + 1);

             A6:

            now

              assume that m > 0 and

               A7: n > 0 ;

              consider k 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));

            end;

             A10:

            now

              assume

               A11: n = 0 ;



              hence ((A |^ m) |^ n) = {( <%> E)} by Th24

              .= (A |^ (m * n)) by A11, Th24;

            end;

            now

              assume

               A12: m = 0 ;



              hence ((A |^ m) |^ n) = ( {( <%> E)} |^ n) by Th24

              .= {( <%> E)} by Th28

              .= (A |^ (m * n)) by A12, Th24;

            end;

            hence ((A |^ m) |^ n) = (A |^ (m * n)) by A10, A6;

          end;

          assume (m + n) <= (l + 1);

          hence ((A |^ m) |^ n) = (A |^ (m * n)) by A4, A3, XXREAL_0: 1;

        end;

        hence P[(l + 1)];

      end;



       A13: P[ 0 ]

      proof

        let m, n;

        assume

         A14: (m + n) <= 0 ;

        then

         A15: m = 0 ;

        n = 0 by A14;



        hence ((A |^ m) |^ n) = {( <%> E)} by Th24

        .= (A |^ (m * n)) by A15, Th24;

      end;



       A16: for l holds P[l] from NAT_1:sch 2( A13, A1);

      now

        let m, n;

        reconsider l = (m + n) as Nat;

        (m + n) <= l;

        hence ((A |^ m) |^ n) = (A |^ (m * n)) by A16;

      end;

      hence thesis;

    end;

    theorem :: FLANG_1:35



     Th35: ( <%> E) in A & n > 0 implies A c= (A |^ n)

    proof

      assume that

       A1: ( <%> E) in A and

       A2: n > 0 ;

      consider m 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 thesis by A3, Th23;

    end;

    theorem :: FLANG_1:36

    ( <%> E) in A & m > n implies (A |^ n) c= (A |^ m)

    proof

      assume that

       A1: ( <%> E) in A and

       A2: m > n;

      consider k 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 thesis by A3, Th33;

    end;

    theorem :: FLANG_1:37



     Th37: A c= B implies (A |^ n) c= (B |^ n)

    proof

      defpred P[ Nat] means (A |^ $1) c= (B |^ $1);

      assume

       A1: A c= B;

       A2:

      now

        let n;

        assume

         A3: P[n];

        ((A |^ n) ^^ A) = (A |^ (n + 1)) & ((B |^ n) ^^ B) = (B |^ (n + 1)) by Th23;

        hence P[(n + 1)] by A1, A3, Th17;

      end;

      (A |^ 0 ) = {( <%> E)} by Th24;

      then

       A4: P[ 0 ] by Th24;

      for n holds P[n] from NAT_1:sch 2( A4, A2);

      hence thesis;

    end;

    theorem :: FLANG_1:38

    ((A |^ n) \/ (B |^ n)) c= ((A \/ B) |^ n)

    proof

      (A |^ n) c= ((A \/ B) |^ n) & (B |^ n) c= ((A \/ B) |^ n) by Th37, XBOOLE_1: 7;

      hence thesis by XBOOLE_1: 8;

    end;

    theorem :: FLANG_1:39

    ((A /\ B) |^ n) c= ((A |^ n) /\ (B |^ n))

    proof

      ((A /\ B) |^ n) c= (A |^ n) & ((A /\ B) |^ n) c= (B |^ n) by Th37, XBOOLE_1: 17;

      hence thesis by XBOOLE_1: 19;

    end;

    theorem :: FLANG_1:40



     Th40: a in (C |^ m) & b in (C |^ n) implies (a ^ b) in (C |^ (m + n))

    proof

      assume a in (C |^ m) & b in (C |^ n);

      then (a ^ b) in ((C |^ m) ^^ (C |^ n)) by Def1;

      hence thesis by Th33;

    end;

    begin

    definition

      let E, A;

      :: FLANG_1:def3

      func A * -> Subset of (E ^omega ) equals ( union { B : ex n st B = (A |^ n) });

      coherence

      proof

        defpred P[ set] means ex n st $1 = (A |^ n);

        reconsider M = { B : P[B] } as Subset-Family of (E ^omega ) from DOMAIN_1:sch 7;

        ( union M) is Subset of (E ^omega );

        hence thesis;

      end;

    end

    theorem :: FLANG_1:41



     Th41: x in (A * ) iff ex n st x in (A |^ n)

    proof

      thus x in (A * ) implies ex n st x in (A |^ n)

      proof

        defpred P[ set] means ex k st $1 = (A |^ k);

        assume x in (A * );

        then

        consider X such that

         A1: x in X and

         A2: X in { B : ex k st B = (A |^ k) } by TARSKI:def 4;



         A3: X in { B : P[B] } by A2;

         P[X] from CARD_FIL:sch 1( A3);

        hence thesis by A1;

      end;

      given n such that

       A4: x in (A |^ n);

      defpred P[ set] means ex k st $1 = (A |^ k);

      consider B such that

       A5: x in B and

       A6: P[B] by A4;

      reconsider A = { C : P[C] } as Subset-Family of (E ^omega ) from DOMAIN_1:sch 7;

      B in A by A6;

      hence thesis by A5, TARSKI:def 4;

    end;

    theorem :: FLANG_1:42



     Th42: (A |^ n) c= (A * )

    proof

      (A |^ n) in { B : ex k st B = (A |^ k) };

      hence thesis by ZFMISC_1: 74;

    end;

    theorem :: FLANG_1:43



     Th43: A c= (A * )

    proof

      A = (A |^ 1) by Th25;

      hence thesis by Th42;

    end;

    theorem :: FLANG_1:44

    (A ^^ A) c= (A * )

    proof

      (A ^^ A) = (A |^ 2) by Th26;

      hence thesis by Th42;

    end;

    theorem :: FLANG_1:45



     Th45: a in (C * ) & b in (C * ) implies (a ^ b) in (C * )

    proof

      assume that

       A1: a in (C * ) and

       A2: b in (C * );

      consider k such that

       A3: a in (C |^ k) by A1, Th41;

      consider l such that

       A4: b in (C |^ l) by A2, Th41;

      (a ^ b) in (C |^ (k + l)) by A3, A4, Th40;

      hence thesis by Th41;

    end;

    theorem :: FLANG_1:46



     Th46: A c= (C * ) & B c= (C * ) implies (A ^^ B) c= (C * )

    proof

      assume

       A1: A c= (C * ) & B c= (C * );

      thus thesis

      proof

        let x be object;

        assume x in (A ^^ B);

        then ex a, b st a in A & b in B & x = (a ^ b) by Def1;

        hence thesis by A1, Th45;

      end;

    end;

    theorem :: FLANG_1:47

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

    proof

      thus (A * ) = {( <%> E)} implies A = {} or A = {( <%> E)}

      proof



         A1: A c= (A * ) by Th43;

        assume that

         A2: (A * ) = {( <%> E)} and

         A3: A <> {} & A <> {( <%> E)};

        ex x be object st x in A & x <> ( <%> E) by A3, ZFMISC_1: 35;

        hence contradiction by A2, A1, TARSKI:def 1;

      end;

       A4:

      now

        assume

         A5: A = {} ;

         A6:

        now

          let x be object;

          assume x in (A * );

          then

          consider n 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;

        end;

        now

          let x be object;

          assume x in {( <%> E)};

          then x in (A |^ 0 ) by Th24;

          hence x in (A * ) by Th41;

        end;

        hence (A * ) = {( <%> E)} by A6, TARSKI: 2;

      end;

      now

        assume

         A8: A = {( <%> E)};



         A9: (A * ) c= {( <%> E)}

        proof

          let x be object;

          assume x in (A * );

          then ex n st x in (A |^ n) by Th41;

          hence thesis by A8, Th28;

        end;

         {( <%> E)} c= (A * )

        proof

          let x be object;

          assume x in {( <%> E)};

          then x in (A |^ 0 ) by Th24;

          hence thesis by Th41;

        end;

        hence (A * ) = {( <%> E)} by A9, XBOOLE_0:def 10;

      end;

      hence thesis by A4;

    end;

    theorem :: FLANG_1:48



     Th48: ( <%> E) in (A * )

    proof

       {( <%> E)} = (A |^ 0 ) by Th24;

      then ( <%> E) in (A |^ 0 ) by TARSKI:def 1;

      hence thesis by Th41;

    end;

    theorem :: FLANG_1:49

    (A * ) = {x} implies x = ( <%> E)

    proof

      assume that

       A1: (A * ) = {x} and

       A2: x <> ( <%> E);

      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 thesis by A1, A3, TARSKI:def 1;

    end;

    theorem :: FLANG_1:50



     Th50: x in (A |^ (m + 1)) implies x in ((A * ) ^^ A) & x in (A ^^ (A * ))

    proof

      assume x in (A |^ (m + 1));

      then

       A1: x in ((A |^ m) ^^ A) by Th23;

      then

      consider a, b 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;

      x in (A ^^ (A |^ m)) by A1, Th32;

      then

      consider a, b 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 thesis by A4, A6, Def1;

    end;

    theorem :: FLANG_1:51

    (A |^ (m + 1)) c= ((A * ) ^^ A) & (A |^ (m + 1)) c= (A ^^ (A * )) by Th50;

    theorem :: FLANG_1:52



     Th52: x in ((A * ) ^^ A) or x in (A ^^ (A * )) implies x in (A * )

    proof

       A1:

      now

        let x;

        assume x in (A ^^ (A * ));

        then

        consider a, b such that

         A2: a in A and

         A3: b in (A * ) and

         A4: x = (a ^ b) by Def1;

        consider n 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;

      end;

      now

        let x;

        assume x in ((A * ) ^^ A);

        then

        consider a, b such that

         A6: a in (A * ) and

         A7: b in A and

         A8: x = (a ^ b) by Def1;

        consider n 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;

      end;

      hence thesis by A1;

    end;

    theorem :: FLANG_1:53

    ((A * ) ^^ A) c= (A * ) & (A ^^ (A * )) c= (A * ) by Th52;

    theorem :: FLANG_1:54



     Th54: ( <%> E) in A implies (A * ) = ((A * ) ^^ A) & (A * ) = (A ^^ (A * ))

    proof

      assume

       A1: ( <%> E) in A;



       A2: ( <%> E) in (A * ) by Th48;

       A3:

      now

        let x;

        assume x in (A * );

        then

        consider n such that

         A4: x in (A |^ n) by Th41;

         A5:

        now

          assume n = 0 ;

          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;

        end;

         A6:

        now

          assume n > 0 ;

          then ex m st (m + 1) = n by NAT_1: 6;

          hence x in (A ^^ (A * )) by A4, Th50;

        end;

        now

          assume n > 0 ;

          then ex m st (m + 1) = n by NAT_1: 6;

          hence x in ((A * ) ^^ A) by A4, Th50;

        end;

        hence x in ((A * ) ^^ A) & x in (A ^^ (A * )) by A5, A6;

      end;

      then

       A7: for x be object holds x in (A * ) implies x in ((A * ) ^^ A);



       A8: for x be object holds x in (A * ) implies x in (A ^^ (A * )) by A3;

      for x be object holds (x in ((A * ) ^^ A) implies x in (A * )) & (x in (A ^^ (A * )) implies x in (A * )) by Th52;

      hence thesis by A7, A8, TARSKI: 2;

    end;

    theorem :: FLANG_1:55

    ( <%> E) in A implies (A * ) = ((A * ) ^^ (A |^ n)) & (A * ) = ((A |^ n) ^^ (A * ))

    proof

      defpred P[ 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;

       A3:

      now

        let n;

        assume

         A4: P[n];



         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 P[(n + 1)] by A5;

      end;

      ((A * ) ^^ (A |^ 0 )) = ((A * ) ^^ {( <%> E)}) by Th24

      .= (A * ) by Th13;

      then

       A6: P[ 0 ] by A1;

      for n holds P[n] from NAT_1:sch 2( A6, A3);

      hence thesis;

    end;

    theorem :: FLANG_1:56



     Th56: (A * ) = ( {( <%> E)} \/ (A ^^ (A * ))) & (A * ) = ( {( <%> E)} \/ ((A * ) ^^ A))

    proof

       A1:

      now

        let x be object;

        assume x in ( {( <%> E)} \/ ((A * ) ^^ 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;

      end;

       A2:

      now

        let x be object;

        assume x in (A * );

        then

        consider n such that

         A3: x in (A |^ n) by Th41;

         A4:

        now

          assume n > 0 ;

          then ex m st (m + 1) = n by NAT_1: 6;

          hence x in ((A * ) ^^ A) by A3, Th50;

        end;

        n = 0 implies x in {( <%> E)} by A3, Th24;

        hence x in ( {( <%> E)} \/ ((A * ) ^^ A)) by A4, XBOOLE_0:def 3;

      end;

       A5:

      now

        let x be object;

        assume x in (A * );

        then

        consider n such that

         A6: x in (A |^ n) by Th41;

         A7:

        now

          assume n > 0 ;

          then ex m st (m + 1) = n by NAT_1: 6;

          hence x in (A ^^ (A * )) by A6, Th50;

        end;

        n = 0 implies x in {( <%> E)} by A6, Th24;

        hence x in ( {( <%> E)} \/ (A ^^ (A * ))) by A7, XBOOLE_0:def 3;

      end;

      now

        let x be object;

        assume x in ( {( <%> E)} \/ (A ^^ (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;

      end;

      hence thesis by A2, A5, A1, TARSKI: 2;

    end;

    theorem :: FLANG_1:57



     Th57: (A ^^ (A * )) = ((A * ) ^^ A)

    proof



       A1: (A * ) = ( {( <%> E)} \/ (A ^^ (A * ))) & (A * ) = ( {( <%> E)} \/ ((A * ) ^^ A)) by Th56;

      now

        per cases ;

          suppose

           A2: ( <%> E) in A;

          then (A * ) = (A ^^ (A * )) by Th54;

          hence thesis by A2, Th54;

        end;

          suppose

           A3: not ( <%> E) in 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 thesis by A1, A4, XBOOLE_1: 71;

        end;

      end;

      hence thesis;

    end;

    theorem :: FLANG_1:58

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

    proof

      defpred P[ Nat] means ((A |^ $1) ^^ (A * )) = ((A * ) ^^ (A |^ $1));

       A1:

      now

        let n;

        assume

         A2: P[n];

        ((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 P[(n + 1)];

      end;

      ((A |^ 0 ) ^^ (A * )) = ( {( <%> E)} ^^ (A * )) by Th24

      .= (A * ) by Th13

      .= ((A * ) ^^ {( <%> E)}) by Th13

      .= ((A * ) ^^ (A |^ 0 )) by Th24;

      then

       A3: P[ 0 ];

      for n holds P[n] from NAT_1:sch 2( A3, A1);

      hence thesis;

    end;

    theorem :: FLANG_1:59



     Th59: A c= (B * ) implies (A |^ n) c= (B * )

    proof

      defpred P[ Nat] means (A |^ $1) c= (B * );

      assume

       A1: A c= (B * );

       A2:

      now

        let n;

        assume P[n];

        then ((A |^ n) ^^ A) c= (B * ) by A1, Th46;

        hence P[(n + 1)] by Th23;

      end;

      ( <%> E) in (B * ) by Th48;

      then {( <%> E)} c= (B * ) by ZFMISC_1: 31;

      then

       A3: P[ 0 ] by Th24;

      for n holds P[n] from NAT_1:sch 2( A3, A2);

      hence thesis;

    end;

    theorem :: FLANG_1:60



     Th60: A c= (B * ) implies (A * ) c= (B * )

    proof

      assume

       A1: A c= (B * );

      thus thesis

      proof

        let x be object;

        assume x in (A * );

        then

        consider n such that

         A2: x in (A |^ n) by Th41;

        (A |^ n) c= (B * ) by A1, Th59;

        hence thesis by A2;

      end;

    end;

    theorem :: FLANG_1:61



     Th61: A c= B implies (A * ) c= (B * )

    proof

      assume

       A1: A c= B;

      B c= (B * ) by Th43;

      then A c= (B * ) by A1;

      hence thesis by Th60;

    end;

    theorem :: FLANG_1:62



     Th62: ((A * ) * ) = (A * )

    proof

      ((A * ) * ) c= (A * ) & (A * ) c= ((A * ) * ) by Th43, Th60;

      hence thesis by XBOOLE_0:def 10;

    end;

    theorem :: FLANG_1:63

    ((A * ) ^^ (A * )) = (A * )

    proof

      ( <%> E) in (A * ) by Th48;

      then

       A1: (A * ) c= ((A * ) ^^ (A * )) by Th16;

      ((A * ) ^^ (A * )) c= (A * ) by Th46;

      hence thesis by A1, XBOOLE_0:def 10;

    end;

    theorem :: FLANG_1:64

    ((A |^ n) * ) c= (A * ) by Th42, Th60;

    theorem :: FLANG_1:65



     Th65: ((A * ) |^ n) c= (A * )

    proof

      ((A * ) |^ n) c= ((A * ) * ) by Th42;

      hence thesis by Th62;

    end;

    theorem :: FLANG_1:66

    n > 0 implies ((A * ) |^ n) = (A * )

    proof

      ( <%> E) in (A * ) by Th48;

      then

       A1: n > 0 implies (A * ) c= ((A * ) |^ n) by Th35;

      ((A * ) |^ n) c= (A * ) by Th65;

      hence thesis by A1, XBOOLE_0:def 10;

    end;

    theorem :: FLANG_1:67



     Th67: A c= (B * ) implies (B * ) = ((B \/ A) * )

    proof

      defpred P[ Nat] means ((B \/ A) |^ $1) c= (B * );

      assume

       A1: A c= (B * );

       A2:

      now

        let n;

        assume

         A3: P[n];

        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 P[(n + 1)] by A3, A4, Th46;

      end;

      ((B \/ A) |^ 0 ) = {( <%> E)} & ( <%> E) in (B * ) by Th24, Th48;

      then

       A5: P[ 0 ] by ZFMISC_1: 31;



       A6: for n holds P[n] from NAT_1:sch 2( A5, A2);



       A7: ((B \/ A) * ) c= (B * )

      proof

        let x be object;

        assume x in ((B \/ A) * );

        then

        consider n such that

         A8: x in ((B \/ A) |^ n) by Th41;

        ((B \/ A) |^ n) c= (B * ) by A6;

        hence thesis by A8;

      end;

      (B * ) c= ((B \/ A) * ) by Th61, XBOOLE_1: 7;

      hence thesis by A7, XBOOLE_0:def 10;

    end;

    theorem :: FLANG_1:68



     Th68: a in (A * ) implies (A * ) = ((A \/ {a}) * ) by ZFMISC_1: 31, Th67;

    theorem :: FLANG_1:69

    (A * ) = ((A \ {( <%> E)}) * )

    proof



      thus ((A \ {( <%> E)}) * ) = (((A \ {( <%> E)}) \/ {( <%> E)}) * ) by Th48, Th68

      .= ((A \/ {( <%> E)}) * ) by XBOOLE_1: 39

      .= (A * ) by Th48, Th68;

    end;

    theorem :: FLANG_1:70

    ((A * ) \/ (B * )) c= ((A \/ B) * )

    proof

      (A * ) c= ((A \/ B) * ) & (B * ) c= ((A \/ B) * ) by Th61, XBOOLE_1: 7;

      hence thesis by XBOOLE_1: 8;

    end;

    theorem :: FLANG_1:71

    ((A /\ B) * ) c= ((A * ) /\ (B * ))

    proof

      ((A /\ B) * ) c= (A * ) & ((A /\ B) * ) c= (B * ) by Th61, XBOOLE_1: 17;

      hence thesis by XBOOLE_1: 19;

    end;

    theorem :: FLANG_1:72



     Th72: <%x%> in (A * ) iff <%x%> in A

    proof

      thus <%x%> in (A * ) implies <%x%> in A

      proof

        defpred P[ Nat] means <%x%> in (A |^ $1);

        assume that

         A1: <%x%> in (A * ) and

         A2: not <%x%> in A;



         A3: ex i be Nat st P[i] by A1, Th41;

        ex n1 be Nat st P[n1] & for n2 be Nat st P[n2] holds n1 <= n2 from NAT_1:sch 5( A3);

        then

        consider n1 be Nat such that

         A4: P[n1] and

         A5: for n2 be Nat st P[n2] holds n1 <= n2;

         A6:

        now

          assume n1 = 0 ;

          then <%x%> in {( <%> E)} by A4, Th24;

          hence contradiction by TARSKI:def 1;

        end;

         A7:

        now

          assume n1 > 1;

          then

          consider n2 such that

           A8: (n2 + 1) = n1 by NAT_1: 6;

           <%x%> in ((A |^ n2) ^^ A) by A4, A8, Th23;

          then

          consider a, b such that

           A9: a in (A |^ n2) and

           A10: b in A & <%x%> = (a ^ b) by Def1;

          now

            reconsider n2 as Element of NAT by ORDINAL1:def 12;

            assume that

             A11: a = <%x%> and b = ( <%> E);

            ex i be Element of NAT st P[i] & n1 > i

            proof

              take n2;

              thus thesis by A8, A9, A11, NAT_1: 13;

            end;

            hence contradiction by A5;

          end;

          hence <%x%> in A by A10, Th4;

        end;

        n1 = 1 implies <%x%> in A by A4, Th25;

        hence contradiction by A2, A7, A6, NAT_1: 25;

      end;

      assume <%x%> in A;

      then <%x%> in (A |^ 1) by Th25;

      hence thesis by Th41;

    end;

    begin

    definition

      let E;

      :: FLANG_1:def4

      func Lex (E) -> Subset of (E ^omega ) means

      : Def4: x in it iff ex e st e in E & x = <%e%>;

      existence

      proof

        defpred P[ set] means ex e st e in E & $1 = <%e%>;

        consider C such that

         A1: x in C iff x in (E ^omega ) & P[x] from SUBSET_1:sch 1;

        take C;

        x in C iff ex e st e in E & x = <%e%>

        proof

          thus x in C implies ex e st e in E & x = <%e%> by A1;

          given e such that

           A2: e in E and

           A3: x = <%e%>;

           {e} c= E by A2, ZFMISC_1: 31;

          then ( rng <%e%>) c= E by AFINSQ_1: 33;

          then <%e%> is XFinSequence of E by RELAT_1:def 19;

          then <%e%> is Element of (E ^omega ) by AFINSQ_1:def 7;

          hence thesis by A1, A2, A3;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let C1,C2 be Subset of (E ^omega ) such that

         A4: x in C1 iff ex e st e in E & x = <%e%> and

         A5: x in C2 iff ex e st e in E & x = <%e%>;

        now

          let x be object;

          thus x in C1 implies x in C2

          proof

            assume x in C1;

            then ex e st e in E & x = <%e%> by A4;

            hence thesis by A5;

          end;

          assume x in C2;

          then ex e st e in E & x = <%e%> by A5;

          hence x in C1 by A4;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    theorem :: FLANG_1:73



     Th73: a in (( Lex E) |^ ( len a))

    proof

      defpred P[ Nat] means for a holds ( len a) = $1 implies a in (( Lex E) |^ $1);

       A1:

      now

        let n;

        assume

         A2: P[n];

        now

          let b;

          assume ( len b) = (n + 1);

          then

          consider c, 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;

        end;

        hence P[(n + 1)];

      end;



       A6: P[ 0 ]

      proof

        let a;

        assume ( len a) = 0 ;

        then a = ( <%> E);

        then a in {( <%> E)} by TARSKI:def 1;

        hence thesis by Th24;

      end;

      for n holds P[n] from NAT_1:sch 2( A6, A1);

      hence thesis;

    end;

    theorem :: FLANG_1:74

    (( Lex E) * ) = (E ^omega )

    proof

       A1:

      now

        let x be object;

        assume x in (E ^omega );

        then

        reconsider a = x as Element of (E ^omega );

        a in (( Lex E) |^ ( len a)) by Th73;

        hence x in (( Lex E) * ) by Th41;

      end;

      for x be object st x in (( Lex E) * ) holds x in (E ^omega );

      hence thesis by A1, TARSKI: 2;

    end;

    theorem :: FLANG_1:75

    (A * ) = (E ^omega ) implies ( Lex E) c= A

    proof

      assume

       A1: (A * ) = (E ^omega );

      thus thesis

      proof

        let x be object;

        assume

         A2: x in ( Lex E);

        then ex e st e in E & x = <%e%> by Def4;

        hence thesis by A1, A2, Th72;

      end;

    end;