flang_3.miz



    begin

    reserve E,x,y,X for set;

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

    reserve a,a1,a2,b for Element of (E ^omega );

    reserve i,k,l,m,n for Nat;

    theorem :: FLANG_3:1

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

    proof

      assume

       A1: B c= (A * );

      then

       A2: (B ^^ (A * )) c= ((A * ) ^^ (A * )) by FLANG_1: 17;

      ((A * ) ^^ B) c= ((A * ) ^^ (A * )) by A1, FLANG_1: 17;

      hence thesis by A2, FLANG_1: 63;

    end;

    begin

    definition

      let E, A, n;

      :: FLANG_3:def1

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

      coherence

      proof

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

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

    

     Th2: x in (A |^.. n) iff ex m st n <= m & x in (A |^ m)

    proof

      thus x in (A |^.. n) implies ex m st n <= m & x in (A |^ m)

      proof

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

        assume x in (A |^.. n);

        then

        consider X such that

         A1: x in X and

         A2: X in { B : ex m st n <= m & B = (A |^ m) } 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 m such that

       A4: n <= m and

       A5: x in (A |^ m);

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

      consider B such that

       A6: x in B and

       A7: P[B] by A4, A5;

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

      B in A by A7;

      hence thesis by A6, TARSKI:def 4;

    end;

    theorem :: FLANG_3:3

    

     Th3: n <= m implies (A |^ m) c= (A |^.. n) by Th2;

    theorem :: FLANG_3:4

    

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

    proof

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

      proof

        

         A1: A <> {} implies (A |^.. n) <> {}

        proof

          assume

           A2: A <> {} ;

          now

            let m;

            consider m such that

             A3: n <= m;

            (A |^ m) <> {} by A2, FLANG_1: 27;

            then ex x be object st x in (A |^ m) by XBOOLE_0:def 1;

            hence thesis by A3, Th2;

          end;

          hence thesis;

        end;

        assume that

         A4: (A |^.. n) = {} and

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

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

        proof

          assume n <= 0 ;

          then

           A6: n = 0 ;

          (A |^ 0 ) c= (A |^.. 0 ) by Th3;

          then {( <%> E)} c= (A |^.. 0 ) by FLANG_1: 24;

          hence thesis by A6, ZFMISC_1: 31;

        end;

        hence contradiction by A4, A5, A1;

      end;

      assume that

       A7: n > 0 and

       A8: A = {} ;

      now

        let x be object;

        assume x in (A |^.. n);

        then ex m st n <= m & x in (A |^ m) by Th2;

        hence contradiction by A7, A8, FLANG_1: 27;

      end;

      hence thesis by XBOOLE_0:def 1;

    end;

    theorem :: FLANG_3:5

    

     Th5: m <= n implies (A |^.. n) c= (A |^.. m)

    proof

      assume

       A1: m <= n;

      let x be object;

      assume x in (A |^.. n);

      then

      consider k such that

       A2: n <= k and

       A3: x in (A |^ k) by Th2;

      m <= k by A1, A2, XXREAL_0: 2;

      hence x in (A |^.. m) by A3, Th2;

    end;

    theorem :: FLANG_3:6

    

     Th6: k <= m implies (A |^ (m,n)) c= (A |^.. k)

    proof

      assume

       A1: k <= m;

      let x be object;

      assume x in (A |^ (m,n));

      then

      consider l such that

       A2: m <= l and l <= n and

       A3: x in (A |^ l) by FLANG_2: 19;

      k <= l by A1, A2, XXREAL_0: 2;

      hence x in (A |^.. k) by A3, Th2;

    end;

    theorem :: FLANG_3:7

    

     Th7: m <= (n + 1) implies ((A |^ (m,n)) \/ (A |^.. (n + 1))) = (A |^.. m)

    proof

      assume m <= (n + 1);

      then

       A1: (A |^.. (n + 1)) c= (A |^.. m) by Th5;

      now

        let x be object;

        assume x in (A |^.. m);

        then

        consider k such that

         A2: m <= k and

         A3: x in (A |^ k) by Th2;

         A4:

        now

          assume k > n;

          then k >= (n + 1) by NAT_1: 13;

          hence x in (A |^.. (n + 1)) by A3, Th2;

        end;

        k <= n implies x in (A |^ (m,n)) by A2, A3, FLANG_2: 19;

        hence x in ((A |^ (m,n)) \/ (A |^.. (n + 1))) by A4, XBOOLE_0:def 3;

      end;

      then

       A5: (A |^.. m) c= ((A |^ (m,n)) \/ (A |^.. (n + 1)));

      (A |^ (m,n)) c= (A |^.. m) by Th6;

      then ((A |^ (m,n)) \/ (A |^.. (n + 1))) c= (A |^.. m) by A1, XBOOLE_1: 8;

      hence thesis by A5, XBOOLE_0:def 10;

    end;

    theorem :: FLANG_3:8

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

    proof

      

       A1: n <= (n + 1) by NAT_1: 13;

      

      thus ((A |^ n) \/ (A |^.. (n + 1))) = ((A |^ (n,n)) \/ (A |^.. (n + 1))) by FLANG_2: 22

      .= (A |^.. n) by A1, Th7;

    end;

    theorem :: FLANG_3:9

    

     Th9: (A |^.. n) c= (A * )

    proof

      let x be object;

      assume x in (A |^.. n);

      then ex k st n <= k & x in (A |^ k) by Th2;

      hence x in (A * ) by FLANG_1: 41;

    end;

    theorem :: FLANG_3:10

    

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

    proof

      thus ( <%> E) in (A |^.. n) implies n = 0 or ( <%> E) in A

      proof

        assume ( <%> E) in (A |^.. n);

        then

         A1: ex k st n <= k & ( <%> E) in (A |^ k) by Th2;

        n = 0 or n > 0 ;

        hence thesis by A1, FLANG_1: 31;

      end;

      assume

       A2: n = 0 or ( <%> E) in A;

      per cases by A2;

        suppose

         A3: n = 0 ;

         {( <%> E)} = (A |^ 0 ) by FLANG_1: 24;

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

        hence thesis by Th2;

      end;

        suppose ( <%> E) in A;

        then ( <%> E) in (A |^ n) by FLANG_1: 30;

        hence thesis by Th2;

      end;

    end;

    theorem :: FLANG_3:11

    

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

    proof

      thus (A |^.. n) = (A * ) implies ( <%> E) in A or n = 0 by FLANG_1: 48, Th10;

      assume

       A1: ( <%> E) in A or n = 0 ;

      now

        let x be object;

        assume x in (A * );

        then

        consider k such that

         A2: x in (A |^ k) by FLANG_1: 41;

        per cases ;

          suppose n <= k;

          hence x in (A |^.. n) by A2, Th2;

        end;

          suppose k < n;

          then (A |^ k) c= (A |^ n) by A1, FLANG_1: 36;

          hence x in (A |^.. n) by A2, Th2;

        end;

      end;

      then

       A3: (A * ) c= (A |^.. n);

      (A |^.. n) c= (A * ) by Th9;

      hence thesis by A3, XBOOLE_0:def 10;

    end;

    theorem :: FLANG_3:12

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

    proof

      

      thus (A * ) = (A |^.. 0 ) by Th11

      .= ((A |^ ( 0 ,n)) \/ (A |^.. (n + 1))) by Th7;

    end;

    theorem :: FLANG_3:13

    

     Th13: A c= B implies (A |^.. n) c= (B |^.. n)

    proof

      assume

       A1: A c= B;

      let x be object;

      assume x in (A |^.. n);

      then

      consider k such that

       A2: n <= k and

       A3: x in (A |^ k) by Th2;

      (A |^ k) c= (B |^ k) by A1, FLANG_1: 37;

      hence x in (B |^.. n) by A2, A3, Th2;

    end;

    theorem :: FLANG_3:14

    

     Th14: x in A & x <> ( <%> E) implies (A |^.. n) <> {( <%> E)}

    proof

      assume that

       A1: x in A and

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

      per cases ;

        suppose

         A3: n = 0 ;

        x in (A |^ 1) by A1, FLANG_1: 25;

        then x in (A |^.. n) by A3, Th2;

        hence thesis by A2, TARSKI:def 1;

      end;

        suppose

         A4: n > 0 ;

        

         A5: (A |^ n) <> {} by A1, FLANG_1: 27;

        (A |^ n) <> {( <%> E)} by A1, A2, A4, FLANG_2: 7;

        then

        consider y be object such that

         A6: y in (A |^ n) and

         A7: y <> ( <%> E) by A5, ZFMISC_1: 35;

        y in (A |^.. n) by A6, Th2;

        hence thesis by A7, TARSKI:def 1;

      end;

    end;

    theorem :: FLANG_3:15

    

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

    proof

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

      proof

        assume that

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

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

         A3: n <> 0 or A <> {} ;

        per cases by A3;

          suppose

           A4: n <> 0 ;

          ( <%> E) in (A |^.. n) by A1, ZFMISC_1: 31;

          then

          consider k such that

           A5: n <= k and

           A6: ( <%> E) in (A |^ k) by Th2;

          k > 0 by A4, A5;

          then

           A7: ( <%> E) in A by A6, FLANG_1: 31;

           not ex x be object st x in A & x <> ( <%> E) by A1, Th14;

          hence contradiction by A2, A7, ZFMISC_1: 35;

        end;

          suppose A <> {} ;

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

          hence contradiction by A1, Th14;

        end;

      end;

      assume

       A8: A = {( <%> E)} or n = 0 & A = {} ;

      per cases by A8;

        suppose

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

         A10:

        now

          let x be object;

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

          then x in (A |^ n) by A9, FLANG_1: 28;

          hence x in (A |^.. n) by Th2;

        end;

        now

          let x be object;

          assume x in (A |^.. n);

          then ex k st n <= k & x in (A |^ k) by Th2;

          hence x in {( <%> E)} by A9, FLANG_1: 28;

        end;

        hence thesis by A10, TARSKI: 2;

      end;

        suppose

         A11: n = 0 & A = {} ;

        

        hence (A |^.. n) = (A * ) by Th11

        .= {( <%> E)} by A11, FLANG_1: 47;

      end;

    end;

    theorem :: FLANG_3:16

    

     Th16: (A |^.. (n + 1)) = ((A |^.. n) ^^ A)

    proof

      now

        let x be object;

        assume x in (A |^.. (n + 1));

        then

        consider k such that

         A1: (n + 1) <= k and

         A2: x in (A |^ k) by Th2;

        consider l such that

         A3: (l + 1) = k by A1, NAT_1: 6;

        x in ((A |^ l) ^^ (A |^ 1)) by A2, A3, FLANG_1: 33;

        then

        consider a, b such that

         A4: a in (A |^ l) and

         A5: b in (A |^ 1) and

         A6: x = (a ^ b) by FLANG_1:def 1;

        n <= l by A1, A3, XREAL_1: 6;

        then a in (A |^.. n) by A4, Th2;

        then x in ((A |^.. n) ^^ (A |^ 1)) by A5, A6, FLANG_1:def 1;

        hence x in ((A |^.. n) ^^ A) by FLANG_1: 25;

      end;

      then

       A7: (A |^.. (n + 1)) c= ((A |^.. n) ^^ A);

      now

        let x be object;

        assume x in ((A |^.. n) ^^ A);

        then

        consider a, b such that

         A8: a in (A |^.. n) and

         A9: b in A and

         A10: x = (a ^ b) by FLANG_1:def 1;

        consider k such that

         A11: n <= k and

         A12: a in (A |^ k) by A8, Th2;

        

         A13: (n + 1) <= (k + 1) by A11, XREAL_1: 6;

        b in (A |^ 1) by A9, FLANG_1: 25;

        then x in (A |^ (k + 1)) by A10, A12, FLANG_1: 40;

        hence x in (A |^.. (n + 1)) by A13, Th2;

      end;

      then ((A |^.. n) ^^ A) c= (A |^.. (n + 1));

      hence thesis by A7, XBOOLE_0:def 10;

    end;

    theorem :: FLANG_3:17

    

     Th17: ((A |^.. m) ^^ (A * )) = (A |^.. m)

    proof

      now

        let x be object;

        assume x in ((A |^.. m) ^^ (A * ));

        then

        consider a, b such that

         A1: a in (A |^.. m) and

         A2: b in (A * ) and

         A3: x = (a ^ b) by FLANG_1:def 1;

        consider k such that

         A4: b in (A |^ k) by A2, FLANG_1: 41;

        consider l such that

         A5: m <= l and

         A6: a in (A |^ l) by A1, Th2;

        

         A7: (l + k) >= m by A5, NAT_1: 12;

        (a ^ b) in (A |^ (l + k)) by A4, A6, FLANG_1: 40;

        hence x in (A |^.. m) by A3, A7, Th2;

      end;

      then

       A8: ((A |^.. m) ^^ (A * )) c= (A |^.. m);

      ( <%> E) in (A * ) by FLANG_1: 48;

      then (A |^.. m) c= ((A |^.. m) ^^ (A * )) by FLANG_1: 16;

      hence thesis by A8, XBOOLE_0:def 10;

    end;

    theorem :: FLANG_3:18

    

     Th18: ((A |^.. m) ^^ (A |^.. n)) = (A |^.. (m + n))

    proof

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

       A1:

      now

        let n;

        assume

         A2: P[n];

        ((A |^.. m) ^^ (A |^.. (n + 1))) = ((A |^.. m) ^^ ((A |^.. n) ^^ A)) by Th16

        .= ((A |^.. (m + n)) ^^ A) by A2, FLANG_1: 18

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

        hence P[(n + 1)];

      end;

      ((A |^.. m) ^^ (A |^.. 0 )) = ((A |^.. m) ^^ (A * )) by Th11

      .= (A |^.. (m + 0 )) by Th17;

      then

       A3: P[ 0 ];

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

      hence thesis;

    end;

    theorem :: FLANG_3:19

    

     Th19: n > 0 implies ((A |^.. m) |^ n) = (A |^.. (m * n))

    proof

      defpred P[ Nat] means $1 > 0 implies ((A |^.. m) |^ $1) = (A |^.. (m * $1));

       A1:

      now

        let n;

        assume

         A2: P[n];

        now

          assume (n + 1) > 0 ;

          per cases ;

            suppose n = 0 ;

            hence ((A |^.. m) |^ (n + 1)) = (A |^.. (m * (n + 1))) by FLANG_1: 25;

          end;

            suppose n > 0 ;

            

            hence ((A |^.. m) |^ (n + 1)) = ((A |^.. (m * n)) ^^ (A |^.. m)) by A2, FLANG_1: 23

            .= (A |^.. ((m * n) + m)) by Th18

            .= (A |^.. (m * (n + 1)));

          end;

        end;

        hence P[(n + 1)];

      end;

      

       A3: P[ 0 ];

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

      hence thesis;

    end;

    theorem :: FLANG_3:20

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

    proof

      now

        let x be object;

        assume x in ((A |^.. n) * );

        then

        consider k such that

         A1: x in ((A |^.. n) |^ k) by FLANG_1: 41;

        per cases ;

          suppose k = 0 ;

          then x in (((A |^.. n) |^ 0 ) \/ ((A |^.. n) |^ 1)) by A1, XBOOLE_0:def 3;

          hence x in ((A |^.. n) ? ) by FLANG_2: 75;

        end;

          suppose

           A2: k > 0 ;

          then ((A |^.. n) |^ k) c= (A |^.. (n * k)) by Th19;

          then

          consider l such that

           A3: (n * k) <= l and

           A4: x in (A |^ l) by A1, Th2;

          k >= ( 0 + 1) by A2, NAT_1: 13;

          then (n * k) >= n by XREAL_1: 151;

          then l >= n by A3, XXREAL_0: 2;

          then x in (A |^.. n) by A4, Th2;

          then x in ((A |^.. n) |^ 1) by FLANG_1: 25;

          then x in (((A |^.. n) |^ 0 ) \/ ((A |^.. n) |^ 1)) by XBOOLE_0:def 3;

          hence x in ((A |^.. n) ? ) by FLANG_2: 75;

        end;

      end;

      then

       A5: ((A |^.. n) * ) c= ((A |^.. n) ? );

      ((A |^.. n) ? ) c= ((A |^.. n) * ) by FLANG_2: 86;

      hence thesis by A5, XBOOLE_0:def 10;

    end;

    theorem :: FLANG_3:21

    

     Th21: A c= (C |^.. m) & B c= (C |^.. n) implies (A ^^ B) c= (C |^.. (m + n))

    proof

      assume that

       A1: A c= (C |^.. m) and

       A2: B c= (C |^.. n);

      thus for x be object holds x in (A ^^ B) implies x in (C |^.. (m + n))

      proof

        let x be object;

        assume x in (A ^^ B);

        then

        consider a, b such that

         A3: a in A and

         A4: b in B and

         A5: x = (a ^ b) by FLANG_1:def 1;

        (a ^ b) in ((C |^.. m) ^^ (C |^.. n)) by A1, A2, A3, A4, FLANG_1:def 1;

        hence thesis by A5, Th18;

      end;

    end;

    theorem :: FLANG_3:22

    

     Th22: (A |^.. (n + k)) = ((A |^.. n) ^^ (A |^ k))

    proof

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

       A1:

      now

        let k be Nat;

        assume

         A2: P[k];

        (A |^.. (n + (k + 1))) = (A |^.. ((n + k) + 1))

        .= (((A |^.. n) ^^ (A |^ k)) ^^ A) by A2, Th16

        .= ((A |^.. n) ^^ ((A |^ k) ^^ A)) by FLANG_1: 18

        .= ((A |^.. n) ^^ (A |^ (k + 1))) by FLANG_1: 23;

        hence P[(k + 1)];

      end;

      (A |^.. (n + 0 )) = ((A |^.. n) ^^ {( <%> E)}) by FLANG_1: 13

      .= ((A |^.. n) ^^ (A |^ 0 )) by FLANG_1: 24;

      then

       A3: P[ 0 ];

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

      hence thesis;

    end;

    theorem :: FLANG_3:23

    

     Th23: (A ^^ (A |^.. n)) = ((A |^.. n) ^^ A)

    proof

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

       A1:

      now

        let k be Nat;

        assume

         A2: P[k];

        (A ^^ (A |^.. (k + 1))) = (A ^^ ((A |^.. k) ^^ A)) by Th16

        .= (((A |^.. k) ^^ A) ^^ A) by A2, FLANG_1: 18

        .= ((A |^.. (k + 1)) ^^ A) by Th16;

        hence P[(k + 1)];

      end;

      (A ^^ (A |^.. 0 )) = (A ^^ (A * )) by Th11

      .= ((A * ) ^^ A) by FLANG_1: 57

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

      then

       A3: P[ 0 ];

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

      hence thesis;

    end;

    theorem :: FLANG_3:24

    

     Th24: ((A |^ k) ^^ (A |^.. n)) = ((A |^.. n) ^^ (A |^ k))

    proof

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

       A1:

      now

        let k;

        assume

         A2: P[k];

        ((A |^ (k + 1)) ^^ (A |^.. n)) = (((A |^ k) ^^ A) ^^ (A |^.. n)) by FLANG_1: 23

        .= ((A ^^ (A |^ k)) ^^ (A |^.. n)) by FLANG_1: 32

        .= (A ^^ ((A |^.. n) ^^ (A |^ k))) by A2, FLANG_1: 18

        .= ((A ^^ (A |^.. n)) ^^ (A |^ k)) by FLANG_1: 18

        .= (((A |^.. n) ^^ A) ^^ (A |^ k)) by Th23

        .= ((A |^.. n) ^^ (A ^^ (A |^ k))) by FLANG_1: 18

        .= ((A |^.. n) ^^ ((A |^ k) ^^ A)) by FLANG_1: 32

        .= ((A |^.. n) ^^ (A |^ (k + 1))) by FLANG_1: 23;

        hence P[(k + 1)];

      end;

      ((A |^ 0 ) ^^ (A |^.. n)) = ( {( <%> E)} ^^ (A |^.. n)) by FLANG_1: 24

      .= (A |^.. n) by FLANG_1: 13

      .= ((A |^.. n) ^^ {( <%> E)}) by FLANG_1: 13

      .= ((A |^.. n) ^^ (A |^ 0 )) by FLANG_1: 24;

      then

       A3: P[ 0 ];

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

      hence thesis;

    end;

    theorem :: FLANG_3:25

    

     Th25: ((A |^ (k,l)) ^^ (A |^.. n)) = ((A |^.. n) ^^ (A |^ (k,l)))

    proof

      defpred P[ Nat] means ((A |^ (k,l)) ^^ (A |^.. $1)) = ((A |^.. $1) ^^ (A |^ (k,l)));

       A1:

      now

        let n;

        assume

         A2: P[n];

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

        .= (((A |^.. n) ^^ (A |^ (k,l))) ^^ A) by A2, FLANG_1: 18

        .= ((A |^.. n) ^^ ((A |^ (k,l)) ^^ A)) by FLANG_1: 18

        .= ((A |^.. n) ^^ (A ^^ (A |^ (k,l)))) by FLANG_2: 36

        .= (((A |^.. n) ^^ A) ^^ (A |^ (k,l))) by FLANG_1: 18

        .= ((A |^.. (n + 1)) ^^ (A |^ (k,l))) by Th16;

        hence P[(n + 1)];

      end;

      ((A |^ (k,l)) ^^ (A |^.. 0 )) = ((A |^ (k,l)) ^^ (A * )) by Th11

      .= ((A * ) ^^ (A |^ (k,l))) by FLANG_2: 66

      .= ((A |^.. 0 ) ^^ (A |^ (k,l))) by Th11;

      then

       A3: P[ 0 ];

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

      hence thesis;

    end;

    theorem :: FLANG_3:26

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

    proof

      assume ( <%> E) in B;

      then ( <%> E) in (B |^.. n) by Th10;

      hence thesis by FLANG_1: 16;

    end;

    theorem :: FLANG_3:27

    

     Th27: ((A |^.. m) ^^ (A |^.. n)) = ((A |^.. n) ^^ (A |^.. m))

    proof

      

      thus ((A |^.. m) ^^ (A |^.. n)) = (A |^.. (m + n)) by Th18

      .= ((A |^.. n) ^^ (A |^.. m)) by Th18;

    end;

    theorem :: FLANG_3:28

    

     Th28: A c= (B |^.. k) & n > 0 implies (A |^ n) c= (B |^.. k)

    proof

      assume that

       A1: A c= (B |^.. k) and

       A2: n > 0 ;

      defpred P[ Nat] means $1 > 0 implies (A |^ $1) c= (B |^.. k);

       A3:

      now

        let m;

        assume

         A4: P[m];

        per cases ;

          suppose m <= 0 ;

          then m = 0 ;

          hence P[(m + 1)] by A1, FLANG_1: 25;

        end;

          suppose m > 0 ;

          then ((A |^ m) ^^ A) c= ((B |^.. k) ^^ (B |^.. k)) by A1, A4, FLANG_1: 17;

          then (A |^ (m + 1)) c= ((B |^.. k) ^^ (B |^.. k)) by FLANG_1: 23;

          then

           A5: (A |^ (m + 1)) c= (B |^.. (k + k)) by Th18;

          (B |^.. (k + k)) c= (B |^.. k) by Th5, NAT_1: 11;

          hence P[(m + 1)] by A5, XBOOLE_1: 1;

        end;

      end;

      

       A6: P[ 0 ];

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

      hence thesis by A2;

    end;

    theorem :: FLANG_3:29

    

     Th29: A c= (B |^.. k) & n > 0 implies (A |^.. n) c= (B |^.. k)

    proof

      assume that

       A1: A c= (B |^.. k) and

       A2: n > 0 ;

      let x be object;

      assume x in (A |^.. n);

      then

      consider m such that

       A3: m >= n and

       A4: x in (A |^ m) by Th2;

      (A |^ m) c= (B |^.. k) by A1, A2, A3, Th28;

      hence thesis by A4;

    end;

    theorem :: FLANG_3:30

    

     Th30: ((A * ) ^^ A) = (A |^.. 1)

    proof

       A1:

      now

        let x be object;

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

        then

        consider a1, a2 such that

         A2: a1 in (A * ) and

         A3: a2 in A and

         A4: x = (a1 ^ a2) by FLANG_1:def 1;

        consider n such that

         A5: a1 in (A |^ n) by A2, FLANG_1: 41;

        

         A6: (n + 1) >= 1 by NAT_1: 11;

        a2 in (A |^ 1) by A3, FLANG_1: 25;

        then (a1 ^ a2) in (A |^ (n + 1)) by A5, FLANG_1: 40;

        hence x in (A |^.. 1) by A4, A6, Th2;

      end;

      now

        let x be object;

        assume x in (A |^.. 1);

        then

        consider n such that

         A7: n >= 1 and

         A8: x in (A |^ n) by Th2;

        consider m such that

         A9: (m + 1) = n by A7, NAT_1: 6;

        (A |^ (m + 1)) c= ((A * ) ^^ A) by FLANG_1: 51;

        hence x in ((A * ) ^^ A) by A8, A9;

      end;

      hence thesis by A1, TARSKI: 2;

    end;

    theorem :: FLANG_3:31

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

    proof

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

       A1:

      now

        let k;

        assume

         A2: P[k];

        ((A * ) ^^ (A |^ (k + 1))) = ((A * ) ^^ ((A |^ k) ^^ A)) by FLANG_1: 23

        .= ((A |^.. k) ^^ A) by A2, FLANG_1: 18

        .= (A |^.. (k + 1)) by Th16;

        hence P[(k + 1)];

      end;

      ((A * ) ^^ (A |^ 0 )) = ((A * ) ^^ {( <%> E)}) by FLANG_1: 24

      .= (A * ) by FLANG_1: 13

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

      then

       A3: P[ 0 ];

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

      hence thesis;

    end;

    theorem :: FLANG_3:32

    

     Th32: ((A |^.. m) ^^ (A * )) = ((A * ) ^^ (A |^.. m))

    proof

      

      thus ((A |^.. m) ^^ (A * )) = ((A |^.. m) ^^ (A |^.. 0 )) by Th11

      .= ((A |^.. 0 ) ^^ (A |^.. m)) by Th27

      .= ((A * ) ^^ (A |^.. m)) by Th11;

    end;

    theorem :: FLANG_3:33

    

     Th33: k <= l implies ((A |^.. n) ^^ (A |^ (k,l))) = (A |^.. (n + k))

    proof

      assume

       A1: k <= l;

      

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

      proof

        let x be object;

        assume x in (A |^.. (n + k));

        then

        consider i such that

         A3: i >= (n + k) and

         A4: x in (A |^ i) by Th2;

        consider m such that

         A5: ((n + k) + m) = i by A3, NAT_1: 10;

        i = ((n + m) + k) by A5;

        then x in ((A |^ (n + m)) ^^ (A |^ k)) by A4, FLANG_1: 33;

        then

         A6: ex a, b st a in (A |^ (n + m)) & b in (A |^ k) & x = (a ^ b) by FLANG_1:def 1;

        

         A7: (A |^ (n + m)) c= (A |^.. n) by Th3, NAT_1: 11;

        (A |^ k) c= (A |^ (k,l)) by A1, FLANG_2: 20;

        hence thesis by A6, A7, FLANG_1:def 1;

      end;

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

      proof

        let x be object;

        assume x in ((A |^.. n) ^^ (A |^ (k,l)));

        then

        consider a, b such that

         A8: a in (A |^.. n) and

         A9: b in (A |^ (k,l)) and

         A10: x = (a ^ b) by FLANG_1:def 1;

        (A |^ (k,l)) c= (A |^.. k) by Th6;

        then (a ^ b) in ((A |^.. n) ^^ (A |^.. k)) by A8, A9, FLANG_1:def 1;

        hence thesis by A10, Th18;

      end;

      hence thesis by A2, XBOOLE_0:def 10;

    end;

    theorem :: FLANG_3:34

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

    proof

      assume k <= l;

      then ((A |^.. 0 ) ^^ (A |^ (k,l))) = (A |^.. ( 0 + k)) by Th33;

      hence thesis by Th11;

    end;

    theorem :: FLANG_3:35

    

     Th35: ((A |^ m) |^.. n) c= (A |^.. (m * n))

    proof

      let x be object;

      assume x in ((A |^ m) |^.. n);

      then

      consider k such that

       A1: k >= n and

       A2: x in ((A |^ m) |^ k) by Th2;

      

       A3: (m * k) >= (m * n) by A1, XREAL_1: 64;

      x in (A |^ (m * k)) by A2, FLANG_1: 34;

      hence thesis by A3, Th2;

    end;

    theorem :: FLANG_3:36

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

    proof

      per cases ;

        suppose

         A1: m > 0 ;

        ((A |^ m) |^.. n) c= (A |^.. (m * n)) by Th35;

        hence thesis by A1, Th19;

      end;

        suppose m <= 0 ;

        then

         A2: m = 0 ;

        

        then ((A |^ m) |^.. n) = ( {( <%> E)} |^.. n) by FLANG_1: 24

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

        .= ((A |^.. n) |^ m) by A2, FLANG_1: 24;

        hence thesis;

      end;

    end;

    theorem :: FLANG_3:37

    

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

    proof

      assume that

       A1: a in (C |^.. m) and

       A2: b in (C |^.. n);

      

       A3: ((C |^.. m) ^^ (C |^.. n)) c= (C |^.. (m + n)) by Th21;

      (a ^ b) in ((C |^.. m) ^^ (C |^.. n)) by A1, A2, FLANG_1:def 1;

      hence thesis by A3;

    end;

    theorem :: FLANG_3:38

    

     Th38: (A |^.. k) = {x} implies x = ( <%> E)

    proof

      assume that

       A1: (A |^.. k) = {x} and

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

      reconsider a = x as Element of (E ^omega ) by A1, ZFMISC_1: 31;

      x in (A |^.. k) by A1, ZFMISC_1: 31;

      then

       A3: (a ^ a) in (A |^.. (k + k)) by Th37;

      

       A4: (A |^.. (k + k)) c= (A |^.. k) by Th5, NAT_1: 11;

      (a ^ a) <> x by A2, FLANG_1: 11;

      hence thesis by A1, A4, A3, TARSKI:def 1;

    end;

    theorem :: FLANG_3:39

    A c= (B * ) implies (A |^.. n) c= (B * )

    proof

      assume

       A1: A c= (B * );

      let x be object;

      assume x in (A |^.. n);

      then

      consider k such that k >= n and

       A2: x in (A |^ k) by Th2;

      (A |^ k) c= (B * ) by A1, FLANG_1: 59;

      hence thesis by A2;

    end;

    theorem :: FLANG_3:40

    

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

    proof

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

      proof

        

         A1: ( <%> E) in (A ? ) by FLANG_2: 78;

        assume (A ? ) c= (A |^.. k);

        hence thesis by A1, Th10;

      end;

      assume k = 0 or ( <%> E) in A;

      then (A |^.. k) = (A * ) by Th11;

      hence thesis by FLANG_2: 86;

    end;

    theorem :: FLANG_3:41

    

     Th41: ((A |^.. k) ^^ (A ? )) = (A |^.. k)

    proof

      

      thus ((A |^.. k) ^^ (A ? )) = ((A |^.. k) ^^ (A |^ ( 0 ,1))) by FLANG_2: 79

      .= (A |^.. (k + 0 )) by Th33

      .= (A |^.. k);

    end;

    theorem :: FLANG_3:42

    ((A |^.. k) ^^ (A ? )) = ((A ? ) ^^ (A |^.. k))

    proof

      

      thus ((A |^.. k) ^^ (A ? )) = ((A |^.. k) ^^ (A |^ ( 0 ,1))) by FLANG_2: 79

      .= ((A |^ ( 0 ,1)) ^^ (A |^.. k)) by Th25

      .= ((A ? ) ^^ (A |^.. k)) by FLANG_2: 79;

    end;

    theorem :: FLANG_3:43

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

    proof

      assume

       A1: B c= (A * );

      then (B ^^ (A |^.. k)) c= ((A * ) ^^ (A |^.. k)) by FLANG_1: 17;

      then

       A2: (B ^^ (A |^.. k)) c= ((A |^.. k) ^^ (A * )) by Th32;

      ((A |^.. k) ^^ B) c= ((A |^.. k) ^^ (A * )) by A1, FLANG_1: 17;

      hence thesis by A2, Th17;

    end;

    theorem :: FLANG_3:44

    

     Th44: ((A /\ B) |^.. k) c= ((A |^.. k) /\ (B |^.. k))

    proof

      let x be object;

      assume x in ((A /\ B) |^.. k);

      then

      consider m such that

       A1: k <= m and

       A2: x in ((A /\ B) |^ m) by Th2;

      

       A3: (B |^ m) c= (B |^.. k) by A1, Th3;

      ((A /\ B) |^ m) c= ((A |^ m) /\ (B |^ m)) by FLANG_1: 39;

      then

       A4: x in ((A |^ m) /\ (B |^ m)) by A2;

      (A |^ m) c= (A |^.. k) by A1, Th3;

      then ((A |^ m) /\ (B |^ m)) c= ((A |^.. k) /\ (B |^.. k)) by A3, XBOOLE_1: 27;

      hence thesis by A4;

    end;

    theorem :: FLANG_3:45

    

     Th45: ((A |^.. k) \/ (B |^.. k)) c= ((A \/ B) |^.. k)

    proof

      let x be object;

      assume

       A1: x in ((A |^.. k) \/ (B |^.. k));

      per cases by A1, XBOOLE_0:def 3;

        suppose x in (A |^.. k);

        then

        consider m such that

         A2: k <= m and

         A3: x in (A |^ m) by Th2;

        

         A4: ((A |^ m) \/ (B |^ m)) c= ((A \/ B) |^ m) by FLANG_1: 38;

        (A |^ m) c= ((A |^ m) \/ (B |^ m)) by XBOOLE_1: 7;

        then (A |^ m) c= ((A \/ B) |^ m) by A4;

        then

         A5: x in ((A \/ B) |^ m) by A3;

        ((A \/ B) |^ m) c= ((A \/ B) |^.. k) by A2, Th3;

        hence thesis by A5;

      end;

        suppose x in (B |^.. k);

        then

        consider m such that

         A6: k <= m and

         A7: x in (B |^ m) by Th2;

        

         A8: ((A |^ m) \/ (B |^ m)) c= ((A \/ B) |^ m) by FLANG_1: 38;

        (B |^ m) c= ((A |^ m) \/ (B |^ m)) by XBOOLE_1: 7;

        then (B |^ m) c= ((A \/ B) |^ m) by A8;

        then

         A9: x in ((A \/ B) |^ m) by A7;

        ((A \/ B) |^ m) c= ((A \/ B) |^.. k) by A6, Th3;

        hence thesis by A9;

      end;

    end;

    theorem :: FLANG_3:46

    

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

    proof

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

      proof

        assume <%x%> in (A |^.. k);

        then ex m st k <= m & <%x%> in (A |^ m) by Th2;

        hence thesis by FLANG_2: 9;

      end;

      assume that

       A1: <%x%> in A and

       A2: ( <%> E) in A or k <= 1;

      per cases by A2, NAT_1: 25;

        suppose ( <%> E) in A & k > 1;

        then <%x%> in (A |^ k) by A1, FLANG_2: 9;

        hence thesis by Th2;

      end;

        suppose k = 0 ;

        then (A |^.. k) = (A * ) by Th11;

        hence thesis by A1, FLANG_1: 72;

      end;

        suppose k = 1;

        then <%x%> in (A |^ k) by A1, FLANG_1: 25;

        hence thesis by Th2;

      end;

    end;

    theorem :: FLANG_3:47

    

     Th47: A c= (B |^.. k) implies (B |^.. k) = ((B \/ A) |^.. k)

    proof

      defpred P[ Nat] means $1 >= k implies ((B \/ A) |^ $1) c= (B |^.. k);

      (B |^ 1) c= (B |^.. 1) by Th3;

      then

       A1: B c= (B |^.. 1) by FLANG_1: 25;

      assume

       A2: A c= (B |^.. k);

       A3:

      now

        let n;

        assume

         A4: P[n];

        now

          assume

           A5: (n + 1) >= k;

          per cases by A5, NAT_1: 8;

            suppose

             A6: (n + 1) = k;

            per cases ;

              suppose k = 0 ;

              hence ((B \/ A) |^ (n + 1)) c= (B |^.. k) by A6;

            end;

              suppose

               A7: k > 0 ;

              then k >= ( 0 + 1) by NAT_1: 13;

              then (B |^.. k) c= (B |^.. 1) by Th5;

              then A c= (B |^.. 1) by A2;

              then (B \/ A) c= (B |^.. 1) by A1, XBOOLE_1: 8;

              then

               A8: ((B \/ A) |^ k) c= ((B |^.. 1) |^ k) by FLANG_1: 37;

              ((B |^.. 1) |^ k) c= (B |^.. (1 * k)) by A7, Th19;

              hence ((B \/ A) |^ (n + 1)) c= (B |^.. k) by A6, A8;

            end;

          end;

            suppose

             A9: n >= k;

            

             A10: (B |^.. (k + k)) c= (B |^.. k) by Th5, NAT_1: 11;

            (((B \/ A) |^ n) ^^ A) c= (B |^.. (k + k)) by A2, A4, A9, Th21;

            then

             A11: (((B \/ A) |^ n) ^^ A) c= (B |^.. k) by A10;

            

             A12: (B |^.. (k + 1)) c= (B |^.. k) by Th5, NAT_1: 11;

            (((B \/ A) |^ n) ^^ B) c= (B |^.. (k + 1)) by A1, A4, A9, Th21;

            then

             A13: (((B \/ A) |^ n) ^^ B) c= (B |^.. k) by A12;

            ((B \/ A) |^ (n + 1)) = (((B \/ A) |^ n) ^^ (B \/ A)) by FLANG_1: 23

            .= ((((B \/ A) |^ n) ^^ B) \/ (((B \/ A) |^ n) ^^ A)) by FLANG_1: 20;

            hence ((B \/ A) |^ (n + 1)) c= (B |^.. k) by A13, A11, XBOOLE_1: 8;

          end;

        end;

        hence P[(n + 1)];

      end;

      

       A14: P[ 0 ]

      proof

        assume 0 >= k;

        then k = 0 ;

        then

         A15: (B |^.. k) = (B * ) by Th11;

        

         A16: ( <%> E) in (B * ) by FLANG_1: 48;

        ((B \/ A) |^ 0 ) = {( <%> E)} by FLANG_1: 24;

        hence thesis by A15, A16, ZFMISC_1: 31;

      end;

      

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

      

       A18: ((B \/ A) |^.. k) c= (B |^.. k)

      proof

        let x be object;

        assume x in ((B \/ A) |^.. k);

        then

        consider n such that

         A19: n >= k and

         A20: x in ((B \/ A) |^ n) by Th2;

        ((B \/ A) |^ n) c= (B |^.. k) by A17, A19;

        hence thesis by A20;

      end;

      (B |^.. k) c= ((B \/ A) |^.. k) by Th13, XBOOLE_1: 7;

      hence thesis by A18, XBOOLE_0:def 10;

    end;

    begin

    definition

      let E, A;

      :: FLANG_3:def2

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

      coherence

      proof

        defpred P[ set] means ex n st n > 0 & $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_3:48

    

     Th48: x in (A + ) iff ex n st n > 0 & x in (A |^ n)

    proof

      thus x in (A + ) implies ex n st n > 0 & x in (A |^ n)

      proof

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

        assume x in (A + );

        then

        consider X such that

         A1: x in X and

         A2: X in { B : ex n st n > 0 & B = (A |^ n) } 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: n > 0 and

       A5: x in (A |^ n);

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

      consider B such that

       A6: x in B and

       A7: P[B] by A4, A5;

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

      B in A by A7;

      hence thesis by A6, TARSKI:def 4;

    end;

    theorem :: FLANG_3:49

    

     Th49: n > 0 implies (A |^ n) c= (A + ) by Th48;

    theorem :: FLANG_3:50

    

     Th50: (A + ) = (A |^.. 1)

    proof

       A1:

      now

        let x be object;

        assume x in (A + );

        then

        consider k such that

         A2: 0 < k and

         A3: x in (A |^ k) by Th48;

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

        hence x in (A |^.. 1) by A3, Th2;

      end;

      now

        let x be object;

        assume x in (A |^.. 1);

        then ex k st 1 <= k & x in (A |^ k) by Th2;

        hence x in (A + ) by Th48;

      end;

      hence thesis by A1, TARSKI: 2;

    end;

    theorem :: FLANG_3:51

    (A + ) = {} iff A = {}

    proof

      (A + ) = (A |^.. 1) by Th50;

      hence thesis by Th4;

    end;

    theorem :: FLANG_3:52

    

     Th52: (A + ) = ((A * ) ^^ A)

    proof

      ((A * ) ^^ A) = (A |^.. 1) by Th30;

      hence thesis by Th50;

    end;

    theorem :: FLANG_3:53

    

     Th53: (A * ) = ( {( <%> E)} \/ (A + ))

    proof

      

      thus (A * ) = ( {( <%> E)} \/ ((A * ) ^^ A)) by FLANG_1: 56

      .= ( {( <%> E)} \/ (A + )) by Th52;

    end;

    theorem :: FLANG_3:54

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

    proof

      

       A1: ( 0 + 1) <= (n + 1) by XREAL_1: 7;

      

      thus (A + ) = (A |^.. 1) by Th50

      .= ((A |^ (1,n)) \/ (A |^.. (n + 1))) by A1, Th7;

    end;

    theorem :: FLANG_3:55

    

     Th55: (A + ) c= (A * )

    proof

      (A |^.. 1) c= (A * ) by Th9;

      hence thesis by Th50;

    end;

    theorem :: FLANG_3:56

    

     Th56: ( <%> E) in (A + ) iff ( <%> E) in A

    proof

      (A + ) = (A |^.. 1) by Th50;

      hence thesis by Th10;

    end;

    theorem :: FLANG_3:57

    

     Th57: (A + ) = (A * ) iff ( <%> E) in A

    proof

      thus (A + ) = (A * ) implies ( <%> E) in A by FLANG_1: 48, Th56;

      assume ( <%> E) in A;

      then (A * ) = ((A * ) ^^ A) by FLANG_1: 54;

      hence thesis by Th52;

    end;

    theorem :: FLANG_3:58

    

     Th58: A c= B implies (A + ) c= (B + )

    proof

      assume A c= B;

      then (A |^.. 1) c= (B |^.. 1) by Th13;

      then (A + ) c= (B |^.. 1) by Th50;

      hence thesis by Th50;

    end;

    theorem :: FLANG_3:59

    

     Th59: A c= (A + )

    proof

      (A |^ 1) c= (A + ) by Th49;

      hence thesis by FLANG_1: 25;

    end;

    theorem :: FLANG_3:60

    

     Th60: ((A * ) + ) = (A * ) & ((A + ) * ) = (A * )

    proof

      

       A1: (A * ) c= ((A + ) * ) by Th59, FLANG_1: 61;

      now

        let x be object;

        assume x in ((A * ) + );

        then

        consider k such that 0 < k and

         A2: x in ((A * ) |^ k) by Th48;

        ((A * ) |^ k) c= (A * ) by FLANG_1: 65;

        hence x in (A * ) by A2;

      end;

      then

       A3: ((A * ) + ) c= (A * );

      now

        let x be object;

        assume x in ((A + ) * );

        then

        consider k such that

         A4: x in ((A + ) |^ k) by FLANG_1: 41;

        ((A + ) |^ k) c= (A * ) by Th55, FLANG_1: 59;

        hence x in (A * ) by A4;

      end;

      then

       A5: ((A + ) * ) c= (A * );

      (A * ) c= ((A * ) + ) by Th59;

      hence thesis by A1, A3, A5, XBOOLE_0:def 10;

    end;

    theorem :: FLANG_3:61

    

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

    proof

      assume A c= (B * );

      then (A + ) c= ((B * ) + ) by Th58;

      hence thesis by Th60;

    end;

    theorem :: FLANG_3:62

    ((A + ) + ) = (A + )

    proof

      now

        let x be object;

        assume that

         A1: x in ((A + ) + );

        per cases ;

          suppose x = ( <%> E);

          hence x in (A + ) by A1, Th56;

        end;

          suppose

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

          ((A + ) + ) c= (A * ) by Th55, Th61;

          then x in (A * ) by A1;

          then

           A3: x in ((A + ) \/ {( <%> E)}) by Th53;

           not x in {( <%> E)} by A2, TARSKI:def 1;

          hence x in (A + ) by A3, XBOOLE_0:def 3;

        end;

      end;

      then

       A4: ((A + ) + ) c= (A + );

      (A + ) c= ((A + ) + ) by Th59;

      hence thesis by A4, XBOOLE_0:def 10;

    end;

    theorem :: FLANG_3:63

    x in A & x <> ( <%> E) implies (A + ) <> {( <%> E)}

    proof

      assume that

       A1: x in A and

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

      (A + ) = (A |^.. 1) by Th50;

      hence thesis by A1, A2, Th14;

    end;

    theorem :: FLANG_3:64

    (A + ) = {( <%> E)} iff A = {( <%> E)}

    proof

      (A + ) = (A |^.. 1) by Th50;

      hence thesis by Th15;

    end;

    theorem :: FLANG_3:65

    ((A + ) ? ) = (A * ) & ((A ? ) + ) = (A * )

    proof

      

      thus ((A + ) ? ) = ( {( <%> E)} \/ (A + )) by FLANG_2: 76

      .= (A * ) by Th53;

      ( <%> E) in (A ? ) by FLANG_2: 78;

      then ((A ? ) + ) = ((A ? ) * ) by Th57;

      hence ((A ? ) + ) = (A * ) by FLANG_2: 85;

    end;

    theorem :: FLANG_3:66

    

     Th66: a in (C + ) & b in (C + ) implies (a ^ b) in (C + )

    proof

      assume that

       A1: a in (C + ) and

       A2: b in (C + );

      consider l such that l > 0 and

       A3: b in (C |^ l) by A2, Th48;

      consider k such that

       A4: k > 0 and

       A5: a in (C |^ k) by A1, Th48;

      (a ^ b) in (C |^ (k + l)) by A5, A3, FLANG_1: 40;

      hence thesis by A4, Th48;

    end;

    theorem :: FLANG_3:67

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

    proof

      assume that

       A1: A c= (C + ) and

       A2: B c= (C + );

      let x be object;

      assume x in (A ^^ B);

      then ex a, b st a in A & b in B & x = (a ^ b) by FLANG_1:def 1;

      hence x in (C + ) by A1, A2, Th66;

    end;

    theorem :: FLANG_3:68

    (A ^^ A) c= (A + )

    proof

      (A ^^ A) = (A |^ 2) by FLANG_1: 26;

      hence thesis by Th49;

    end;

    theorem :: FLANG_3:69

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

    proof

      assume that

       A1: (A + ) = {x} and

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

      (A |^.. 1) = {x} by A1, Th50;

      hence thesis by A2, Th38;

    end;

    theorem :: FLANG_3:70

    (A ^^ (A + )) = ((A + ) ^^ A)

    proof

      

      thus (A ^^ (A + )) = (A ^^ (A |^.. 1)) by Th50

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

      .= ((A + ) ^^ A) by Th50;

    end;

    theorem :: FLANG_3:71

    ((A |^ k) ^^ (A + )) = ((A + ) ^^ (A |^ k))

    proof

      

      thus ((A |^ k) ^^ (A + )) = ((A |^ k) ^^ (A |^.. 1)) by Th50

      .= ((A |^.. 1) ^^ (A |^ k)) by Th24

      .= ((A + ) ^^ (A |^ k)) by Th50;

    end;

    theorem :: FLANG_3:72

    

     Th72: ((A |^ (m,n)) ^^ (A + )) = ((A + ) ^^ (A |^ (m,n)))

    proof

      

      thus ((A |^ (m,n)) ^^ (A + )) = ((A |^ (m,n)) ^^ (A |^.. 1)) by Th50

      .= ((A |^.. 1) ^^ (A |^ (m,n))) by Th25

      .= ((A + ) ^^ (A |^ (m,n))) by Th50;

    end;

    theorem :: FLANG_3:73

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

    proof

      assume ( <%> E) in B;

      then (B + ) = (B * ) by Th57;

      hence thesis by FLANG_2: 18;

    end;

    theorem :: FLANG_3:74

    ((A + ) ^^ (A + )) = (A |^.. 2)

    proof

      

      thus ((A + ) ^^ (A + )) = ((A |^.. 1) ^^ (A + )) by Th50

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

      .= (A |^.. (1 + 1)) by Th18

      .= (A |^.. 2);

    end;

    theorem :: FLANG_3:75

    

     Th75: ((A + ) ^^ (A |^ k)) = (A |^.. (k + 1))

    proof

      

      thus ((A + ) ^^ (A |^ k)) = ((A |^.. 1) ^^ (A |^ k)) by Th50

      .= (A |^.. (k + 1)) by Th22;

    end;

    theorem :: FLANG_3:76

    ((A + ) ^^ A) = (A |^.. 2)

    proof

      ((A + ) ^^ A) = ((A + ) ^^ (A |^ 1)) by FLANG_1: 25

      .= (A |^.. (1 + 1)) by Th75;

      hence thesis;

    end;

    theorem :: FLANG_3:77

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

    proof

      assume k <= l;

      then ((A |^.. 1) ^^ (A |^ (k,l))) = (A |^.. (1 + k)) by Th33;

      hence thesis by Th50;

    end;

    theorem :: FLANG_3:78

    A c= (B + ) & n > 0 implies (A |^ n) c= (B + )

    proof

      assume that

       A1: A c= (B + ) and

       A2: n > 0 ;

      A c= (B |^.. 1) by A1, Th50;

      then (A |^ n) c= (B |^.. 1) by A2, Th28;

      hence thesis by Th50;

    end;

    theorem :: FLANG_3:79

    ((A + ) ^^ (A ? )) = ((A ? ) ^^ (A + ))

    proof

      

      thus ((A + ) ^^ (A ? )) = ((A + ) ^^ (A |^ ( 0 ,1))) by FLANG_2: 79

      .= ((A |^ ( 0 ,1)) ^^ (A + )) by Th72

      .= ((A ? ) ^^ (A + )) by FLANG_2: 79;

    end;

    theorem :: FLANG_3:80

    ((A + ) ^^ (A ? )) = (A + )

    proof

      

      thus ((A + ) ^^ (A ? )) = ((A |^.. 1) ^^ (A ? )) by Th50

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

      .= (A + ) by Th50;

    end;

    theorem :: FLANG_3:81

    (A ? ) c= (A + ) iff ( <%> E) in A

    proof

      (A + ) = (A |^.. 1) by Th50;

      hence thesis by Th40;

    end;

    theorem :: FLANG_3:82

    A c= (B + ) implies (A + ) c= (B + )

    proof

      assume A c= (B + );

      then A c= (B |^.. 1) by Th50;

      then (A |^.. 1) c= (B |^.. 1) by Th29;

      then (A + ) c= (B |^.. 1) by Th50;

      hence thesis by Th50;

    end;

    theorem :: FLANG_3:83

    A c= (B + ) implies (B + ) = ((B \/ A) + )

    proof

      assume A c= (B + );

      then A c= (B |^.. 1) by Th50;

      then (B |^.. 1) = ((B \/ A) |^.. 1) by Th47;

      then (B |^.. 1) = ((B \/ A) + ) by Th50;

      hence thesis by Th50;

    end;

    theorem :: FLANG_3:84

    n > 0 implies (A |^.. n) c= (A + )

    proof

      assume

       A1: n > 0 ;

      let x be object;

      assume x in (A |^.. n);

      then ex k st k >= n & x in (A |^ k) by Th2;

      hence thesis by A1, Th48;

    end;

    theorem :: FLANG_3:85

    m > 0 implies (A |^ (m,n)) c= (A + )

    proof

      assume

       A1: m > 0 ;

      let x be object;

      assume x in (A |^ (m,n));

      then ex k st m <= k & k <= n & x in (A |^ k) by FLANG_2: 19;

      hence thesis by A1, Th48;

    end;

    theorem :: FLANG_3:86

    

     Th86: ((A * ) ^^ (A + )) = ((A + ) ^^ (A * ))

    proof

      

      thus ((A * ) ^^ (A + )) = ((A * ) ^^ (A |^.. 1)) by Th50

      .= ((A |^.. 1) ^^ (A * )) by Th32

      .= ((A + ) ^^ (A * )) by Th50;

    end;

    theorem :: FLANG_3:87

    

     Th87: ((A + ) |^ k) c= (A |^.. k)

    proof

      per cases ;

        suppose k > 0 ;

        then ((A |^.. 1) |^ k) c= (A |^.. (1 * k)) by Th19;

        hence thesis by Th50;

      end;

        suppose

         A1: k = 0 ;

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

        then

         A2: ( <%> E) in (A |^.. 0 ) by FLANG_1: 48;

        ((A + ) |^ k) = {( <%> E)} by A1, FLANG_1: 24;

        hence thesis by A1, A2, ZFMISC_1: 31;

      end;

    end;

    theorem :: FLANG_3:88

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

    proof

      let x be object;

      assume x in ((A + ) |^ (m,n));

      then

      consider k such that

       A1: m <= k and k <= n and

       A2: x in ((A + ) |^ k) by FLANG_2: 19;

      ((A + ) |^ k) c= (A |^.. k) by Th87;

      then

       A3: x in (A |^.. k) by A2;

      (A |^.. k) c= (A |^.. m) by A1, Th5;

      hence thesis by A3;

    end;

    theorem :: FLANG_3:89

    A c= (B + ) & n > 0 implies (A |^.. n) c= (B + )

    proof

      assume that

       A1: A c= (B + ) and

       A2: n > 0 ;

      A c= (B |^.. 1) by A1, Th50;

      then (A |^.. n) c= (B |^.. 1) by A2, Th29;

      hence thesis by Th50;

    end;

    theorem :: FLANG_3:90

    

     Th90: ((A + ) ^^ (A |^.. k)) = (A |^.. (k + 1))

    proof

      

      thus ((A + ) ^^ (A |^.. k)) = ((A |^.. 1) ^^ (A |^.. k)) by Th50

      .= (A |^.. (k + 1)) by Th18;

    end;

    theorem :: FLANG_3:91

    ((A + ) ^^ (A |^.. k)) = ((A |^.. k) ^^ (A + ))

    proof

      

      thus ((A + ) ^^ (A |^.. k)) = (A |^.. (k + 1)) by Th90

      .= ((A |^.. k) ^^ (A |^.. 1)) by Th18

      .= ((A |^.. k) ^^ (A + )) by Th50;

    end;

    theorem :: FLANG_3:92

    

     Th92: ((A + ) ^^ (A * )) = (A + )

    proof

      

      thus ((A + ) ^^ (A * )) = ((A |^.. 1) ^^ (A * )) by Th50

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

      .= (A + ) by Th50;

    end;

    theorem :: FLANG_3:93

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

    proof

      assume

       A1: B c= (A * );

      then (B ^^ (A + )) c= ((A * ) ^^ (A + )) by FLANG_1: 17;

      then

       A2: (B ^^ (A + )) c= ((A + ) ^^ (A * )) by Th86;

      ((A + ) ^^ B) c= ((A + ) ^^ (A * )) by A1, FLANG_1: 17;

      hence thesis by A2, Th92;

    end;

    theorem :: FLANG_3:94

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

    proof

      

       A1: (A + ) = (A |^.. 1) by Th50;

      

       A2: (B + ) = (B |^.. 1) by Th50;

      ((A /\ B) + ) = ((A /\ B) |^.. 1) by Th50;

      hence thesis by A1, A2, Th44;

    end;

    theorem :: FLANG_3:95

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

    proof

      

       A1: (A + ) = (A |^.. 1) by Th50;

      

       A2: (B + ) = (B |^.. 1) by Th50;

      ((A \/ B) + ) = ((A \/ B) |^.. 1) by Th50;

      hence thesis by A1, A2, Th45;

    end;

    theorem :: FLANG_3:96

     <%x%> in (A + ) iff <%x%> in A

    proof

      (A + ) = (A |^.. 1) by Th50;

      hence thesis by Th46;

    end;