member_1.miz

    begin

    reserve w,w1,w2 for Element of ExtREAL ;

    reserve c,c1,c2 for Complex;

    reserve A,B,C,D for complex-membered set;

    reserve F,G,H,I for ext-real-membered set;

    reserve a,b,s,t,z for Complex;

    reserve f,g,h,i,j for ExtReal;

    reserve r for Real;

    reserve e for set;

    definition

      let w;

      :: original: -

      redefine

      func - w -> Element of ExtREAL ;

      coherence by XXREAL_0:def 1;

      :: original: "

      redefine

      func w " -> Element of ExtREAL ;

      coherence by XXREAL_0:def 1;

      let w1;

      :: original: *

      redefine

      func w * w1 -> Element of ExtREAL ;

      coherence by XXREAL_0:def 1;

    end

    registration

      let a,b,c,d be Complex;

      cluster {a, b, c, d} -> complex-membered;

      coherence by ENUMSET1:def 2;

    end

    registration

      let a,b,c,d be ExtReal;

      cluster {a, b, c, d} -> ext-real-membered;

      coherence by ENUMSET1:def 2;

    end

    definition

      let F be ext-real-membered set;

      :: MEMBER_1:def1

      func -- F -> ext-real-membered set equals { ( - w) : w in F };

      coherence

      proof

        { ( - w) : w in F } is ext-real-membered

        proof

          let e be object;

          assume e in { ( - w) : w in F };

          then ex w st e = ( - w) & w in F;

          hence thesis;

        end;

        hence thesis;

      end;

      involutiveness

      proof

        let A,B be ext-real-membered set;

        assume

         A1: A = { ( - w) : w in B };

        thus B c= { ( - w) : w in A }

        proof

          let z be ExtReal;



           A2: z in ExtREAL by XXREAL_0:def 1;



           A3: ( - z) in ExtREAL & z = ( - ( - z)) by XXREAL_0:def 1;

          assume z in B;

          then ( - z) in A by A1, A2;

          hence thesis by A3;

        end;

        let e be object;

        assume e in { ( - w) : w in A };

        then

        consider w1 such that

         A4: ( - w1) = e and

         A5: w1 in A;

        ex w st ( - w) = w1 & w in B by A1, A5;

        hence thesis by A4;

      end;

    end

    theorem :: MEMBER_1:1



     Th1: f in F iff ( - f) in ( -- F)

    proof

      f in ExtREAL by XXREAL_0:def 1;

      hence f in F implies ( - f) in ( -- F);

      assume ( - f) in ( -- F);

      then

       A1: ex w st ( - w) = ( - f) & w in F;

      ( - ( - f)) = f;

      hence thesis by A1;

    end;

    theorem :: MEMBER_1:2



     Th2: ( - f) in F iff f in ( -- F)

    proof

      ( - ( - f)) = f;

      hence thesis by Th1;

    end;

    registration

      let F be empty set;

      cluster ( -- F) -> empty;

      coherence

      proof

        assume ( -- F) is non empty;

        then the Element of ( -- F) in ( -- F);

        then ex w st the Element of ( -- F) = ( - w) & w in F;

        hence thesis;

      end;

    end

    registration

      let F be ext-real-membered non empty set;

      cluster ( -- F) -> non empty;

      coherence

      proof

        ( - the Element of F) in ( -- F) by Th1;

        hence thesis;

      end;

    end



     Lm1: F c= G implies ( -- F) c= ( -- G)

    proof

      assume

       A1: F c= G;

      let j;

      assume j in ( -- F);

      then ( - j) in F by Th2;

      hence thesis by A1, Th2;

    end;

    theorem :: MEMBER_1:3



     Th3: F c= G iff ( -- F) c= ( -- G)

    proof

      ( -- ( -- F)) = F & ( -- ( -- G)) = G;

      hence thesis by Lm1;

    end;

    theorem :: MEMBER_1:4

    ( -- F) = ( -- G) implies F = G

    proof

      assume ( -- F) = ( -- G);

      then F c= G & G c= F by Th3;

      hence thesis;

    end;

    theorem :: MEMBER_1:5



     Th5: ( -- (F \/ G)) = (( -- F) \/ ( -- G))

    proof

      let i;

      hereby

        assume i in ( -- (F \/ G));

        then ( - i) in (F \/ G) by Th2;

        then ( - i) in F or ( - i) in G by XBOOLE_0:def 3;

        then i in ( -- F) or i in ( -- G) by Th2;

        hence i in (( -- F) \/ ( -- G)) by XBOOLE_0:def 3;

      end;

      assume i in (( -- F) \/ ( -- G));

      then i in ( -- F) or i in ( -- G) by XBOOLE_0:def 3;

      then ( - i) in F or ( - i) in G by Th2;

      then ( - i) in (F \/ G) by XBOOLE_0:def 3;

      hence thesis by Th2;

    end;

    theorem :: MEMBER_1:6



     Th6: ( -- (F /\ G)) = (( -- F) /\ ( -- G))

    proof

      let i;

      hereby

        assume i in ( -- (F /\ G));

        then

         A1: ( - i) in (F /\ G) by Th2;

        then ( - i) in G by XBOOLE_0:def 4;

        then

         A2: i in ( -- G) by Th2;

        ( - i) in F by A1, XBOOLE_0:def 4;

        then i in ( -- F) by Th2;

        hence i in (( -- F) /\ ( -- G)) by A2, XBOOLE_0:def 4;

      end;

      assume

       A3: i in (( -- F) /\ ( -- G));

      then i in ( -- G) by XBOOLE_0:def 4;

      then

       A4: ( - i) in G by Th2;

      i in ( -- F) by A3, XBOOLE_0:def 4;

      then ( - i) in F by Th2;

      then ( - i) in (F /\ G) by A4, XBOOLE_0:def 4;

      hence thesis by Th2;

    end;

    theorem :: MEMBER_1:7



     Th7: ( -- (F \ G)) = (( -- F) \ ( -- G))

    proof

      let i;

      hereby

        assume i in ( -- (F \ G));

        then

         A1: ( - i) in (F \ G) by Th2;

        then not ( - i) in G by XBOOLE_0:def 5;

        then

         A2: not i in ( -- G) by Th2;

        i in ( -- F) by A1, Th2;

        hence i in (( -- F) \ ( -- G)) by A2, XBOOLE_0:def 5;

      end;

      assume

       A3: i in (( -- F) \ ( -- G));

      then not i in ( -- G) by XBOOLE_0:def 5;

      then

       A4: not ( - i) in G by Th2;

      ( - i) in F by A3, Th2;

      then ( - i) in (F \ G) by A4, XBOOLE_0:def 5;

      hence thesis by Th2;

    end;

    theorem :: MEMBER_1:8



     Th8: ( -- (F \+\ G)) = (( -- F) \+\ ( -- G))

    proof



      thus ( -- (F \+\ G)) = (( -- (F \ G)) \/ ( -- (G \ F))) by Th5

      .= ((( -- F) \ ( -- G)) \/ ( -- (G \ F))) by Th7

      .= (( -- F) \+\ ( -- G)) by Th7;

    end;

    theorem :: MEMBER_1:9



     Th9: ( -- {f}) = {( - f)}

    proof

      let i;

      hereby

        assume i in ( -- {f});

        then

        consider w such that

         A1: i = ( - w) and

         A2: w in {f};

        w = f by A2, TARSKI:def 1;

        hence i in {( - f)} by A1, TARSKI:def 1;

      end;

      assume i in {( - f)};

      then

       A3: i = ( - f) by TARSKI:def 1;

      f in ExtREAL & f in {f} by TARSKI:def 1, XXREAL_0:def 1;

      hence thesis by A3;

    end;

    theorem :: MEMBER_1:10



     Th10: ( -- {f, g}) = {( - f), ( - g)}

    proof



      thus ( -- {f, g}) = ( -- ( {f} \/ {g})) by ENUMSET1: 1

      .= (( -- {f}) \/ ( -- {g})) by Th5

      .= ( {( - f)} \/ ( -- {g})) by Th9

      .= ( {( - f)} \/ {( - g)}) by Th9

      .= {( - f), ( - g)} by ENUMSET1: 1;

    end;

    definition

      let A be complex-membered set;

      :: MEMBER_1:def2

      func -- A -> complex-membered set equals { ( - c) : c in A };

      coherence

      proof

        { ( - c) : c in A } is complex-membered

        proof

          let e be object;

          assume e in { ( - c) : c in A };

          then ex c st e = ( - c) & c in A;

          hence thesis;

        end;

        hence thesis;

      end;

      involutiveness

      proof

        let A, B;

        assume

         A1: A = { ( - c) : c in B };

        thus B c= { ( - c) : c in A }

        proof

          let z;



           A2: ( - z) in COMPLEX & z = ( - ( - z)) by XCMPLX_0:def 2;

          assume z in B;

          then ( - z) in A by A1;

          hence thesis by A2;

        end;

        let e be object;

        assume e in { ( - c) : c in A };

        then

        consider r0 be Complex such that

         A3: ( - r0) = e and

         A4: r0 in A;

        ex c st ( - c) = r0 & c in B by A1, A4;

        hence thesis by A3;

      end;

    end

    theorem :: MEMBER_1:11



     Th11: a in A iff ( - a) in ( -- A)

    proof

      thus a in A implies ( - a) in ( -- A);

      assume ( - a) in ( -- A);

      then ex c st ( - c) = ( - a) & c in A;

      hence thesis;

    end;

    theorem :: MEMBER_1:12



     Th12: ( - a) in A iff a in ( -- A)

    proof

      ( - ( - a)) = a;

      hence thesis by Th11;

    end;

    registration

      let A be empty set;

      cluster ( -- A) -> empty;

      coherence

      proof

        assume ( -- A) is non empty;

        then the Element of ( -- A) in ( -- A);

        then ex c st the Element of ( -- A) = ( - c) & c in A;

        hence thesis;

      end;

    end

    registration

      let A be complex-membered non empty set;

      cluster ( -- A) -> non empty;

      coherence

      proof

        ( - the Element of A) in ( -- A);

        hence thesis;

      end;

    end

    registration

      let A be real-membered set;

      cluster ( -- A) -> real-membered;

      coherence

      proof

        let e be object;

        assume e in ( -- A);

        then ex c st e = ( - c) & c in A;

        hence thesis;

      end;

    end

    registration

      let A be rational-membered set;

      cluster ( -- A) -> rational-membered;

      coherence

      proof

        let e be object;

        assume e in ( -- A);

        then ex c st e = ( - c) & c in A;

        hence thesis;

      end;

    end

    registration

      let A be integer-membered set;

      cluster ( -- A) -> integer-membered;

      coherence

      proof

        let e be object;

        assume e in ( -- A);

        then ex c st e = ( - c) & c in A;

        hence thesis;

      end;

    end

    registration

      let A be real-membered set, F be ext-real-membered set;

      identify -- F with -- A when A = F;

      compatibility

      proof

        assume

         A1: A = F;

        let a be ExtReal;

        hereby

          assume

           A2: a in ( -- A);

          then

          reconsider b = a as Real;

          ( - b) in A by A2, Th12;

          hence a in ( -- F) by A1, Th2;

        end;

        assume a in ( -- F);

        then

        consider w such that

         A3: a = ( - w) and

         A4: w in F;

        reconsider b = w as Real by A1, A4;

        ( - b) in ( -- A) by A1, A4;

        hence thesis by A3;

      end;

    end



     Lm2: A c= B implies ( -- A) c= ( -- B)

    proof

      assume

       A1: A c= B;

      let a;

      assume a in ( -- A);

      then ( - a) in A by Th12;

      hence thesis by A1, Th12;

    end;

    theorem :: MEMBER_1:13



     Th13: A c= B iff ( -- A) c= ( -- B)

    proof

      ( -- ( -- A)) = A & ( -- ( -- B)) = B;

      hence thesis by Lm2;

    end;

    theorem :: MEMBER_1:14

    ( -- A) = ( -- B) implies A = B

    proof

      assume ( -- A) = ( -- B);

      then A c= B & B c= A by Th13;

      hence thesis;

    end;

    theorem :: MEMBER_1:15



     Th15: ( -- (A \/ B)) = (( -- A) \/ ( -- B))

    proof

      let z;

      hereby

        assume z in ( -- (A \/ B));

        then ( - z) in (A \/ B) by Th12;

        then ( - z) in A or ( - z) in B by XBOOLE_0:def 3;

        then z in ( -- A) or z in ( -- B) by Th12;

        hence z in (( -- A) \/ ( -- B)) by XBOOLE_0:def 3;

      end;

      assume z in (( -- A) \/ ( -- B));

      then z in ( -- A) or z in ( -- B) by XBOOLE_0:def 3;

      then ( - z) in A or ( - z) in B by Th12;

      then ( - z) in (A \/ B) by XBOOLE_0:def 3;

      hence thesis by Th12;

    end;

    theorem :: MEMBER_1:16



     Th16: ( -- (A /\ B)) = (( -- A) /\ ( -- B))

    proof

      let z;

      hereby

        assume z in ( -- (A /\ B));

        then

         A1: ( - z) in (A /\ B) by Th12;

        then ( - z) in B by XBOOLE_0:def 4;

        then

         A2: z in ( -- B) by Th12;

        ( - z) in A by A1, XBOOLE_0:def 4;

        then z in ( -- A) by Th12;

        hence z in (( -- A) /\ ( -- B)) by A2, XBOOLE_0:def 4;

      end;

      assume

       A3: z in (( -- A) /\ ( -- B));

      then z in ( -- B) by XBOOLE_0:def 4;

      then

       A4: ( - z) in B by Th12;

      z in ( -- A) by A3, XBOOLE_0:def 4;

      then ( - z) in A by Th12;

      then ( - z) in (A /\ B) by A4, XBOOLE_0:def 4;

      hence thesis by Th12;

    end;

    theorem :: MEMBER_1:17



     Th17: ( -- (A \ B)) = (( -- A) \ ( -- B))

    proof

      let z;

      hereby

        assume z in ( -- (A \ B));

        then

         A1: ( - z) in (A \ B) by Th12;

        then not ( - z) in B by XBOOLE_0:def 5;

        then

         A2: not z in ( -- B) by Th12;

        z in ( -- A) by A1, Th12;

        hence z in (( -- A) \ ( -- B)) by A2, XBOOLE_0:def 5;

      end;

      assume

       A3: z in (( -- A) \ ( -- B));

      then not z in ( -- B) by XBOOLE_0:def 5;

      then

       A4: not ( - z) in B by Th12;

      ( - z) in A by A3, Th12;

      then ( - z) in (A \ B) by A4, XBOOLE_0:def 5;

      hence thesis by Th12;

    end;

    theorem :: MEMBER_1:18



     Th18: ( -- (A \+\ B)) = (( -- A) \+\ ( -- B))

    proof



      thus ( -- (A \+\ B)) = (( -- (A \ B)) \/ ( -- (B \ A))) by Th15

      .= ((( -- A) \ ( -- B)) \/ ( -- (B \ A))) by Th17

      .= (( -- A) \+\ ( -- B)) by Th17;

    end;

    theorem :: MEMBER_1:19



     Th19: ( -- {a}) = {( - a)}

    proof

      let z;

      hereby

        assume z in ( -- {a});

        then

        consider c such that

         A1: z = ( - c) and

         A2: c in {a};

        c = a by A2, TARSKI:def 1;

        hence z in {( - a)} by A1, TARSKI:def 1;

      end;

      assume z in {( - a)};

      then

       A3: z = ( - a) by TARSKI:def 1;

      a in COMPLEX & a in {a} by TARSKI:def 1, XCMPLX_0:def 2;

      hence thesis by A3;

    end;

    theorem :: MEMBER_1:20



     Th20: ( -- {a, b}) = {( - a), ( - b)}

    proof



      thus ( -- {a, b}) = ( -- ( {a} \/ {b})) by ENUMSET1: 1

      .= (( -- {a}) \/ ( -- {b})) by Th15

      .= ( {( - a)} \/ ( -- {b})) by Th19

      .= ( {( - a)} \/ {( - b)}) by Th19

      .= {( - a), ( - b)} by ENUMSET1: 1;

    end;

    definition

      let F be ext-real-membered set;

      :: MEMBER_1:def3

      func F "" -> ext-real-membered set equals { (w " ) : w in F };

      coherence

      proof

        { (w " ) : w in F } is ext-real-membered

        proof

          let e be object;

          assume e in { (w " ) : w in F };

          then ex w st e = (w " ) & w in F;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    theorem :: MEMBER_1:21



     Th21: f in F implies (f " ) in (F "" )

    proof

      f in ExtREAL by XXREAL_0:def 1;

      hence thesis;

    end;

    registration

      let F be empty set;

      cluster (F "" ) -> empty;

      coherence

      proof

        assume (F "" ) is non empty;

        then the Element of (F "" ) in (F "" );

        then ex w st the Element of (F "" ) = (w " ) & w in F;

        hence thesis;

      end;

    end

    registration

      let F be ext-real-membered non empty set;

      cluster (F "" ) -> non empty;

      coherence

      proof

        ( the Element of F " ) in (F "" ) by Th21;

        hence thesis;

      end;

    end

    theorem :: MEMBER_1:22

    F c= G implies (F "" ) c= (G "" )

    proof

      assume

       A1: F c= G;

      let i;

      assume i in (F "" );

      then ex w st i = (w " ) & w in F;

      hence thesis by A1;

    end;

    theorem :: MEMBER_1:23



     Th23: ((F \/ G) "" ) = ((F "" ) \/ (G "" ))

    proof

      let i;

      hereby

        assume i in ((F \/ G) "" );

        then

        consider w such that

         A1: i = (w " ) and

         A2: w in (F \/ G);

        w in F or w in G by A2, XBOOLE_0:def 3;

        then (w " ) in (F "" ) or (w " ) in (G "" );

        hence i in ((F "" ) \/ (G "" )) by A1, XBOOLE_0:def 3;

      end;

      assume

       A3: i in ((F "" ) \/ (G "" ));

      per cases by A3, XBOOLE_0:def 3;

        suppose i in (F "" );

        then

        consider w such that

         A4: i = (w " ) and

         A5: w in F;

        w in (F \/ G) by A5, XBOOLE_0:def 3;

        hence thesis by A4;

      end;

        suppose i in (G "" );

        then

        consider w such that

         A6: i = (w " ) and

         A7: w in G;

        w in (F \/ G) by A7, XBOOLE_0:def 3;

        hence thesis by A6;

      end;

    end;

    theorem :: MEMBER_1:24



     Th24: ((F /\ G) "" ) c= ((F "" ) /\ (G "" ))

    proof

      let i;

      assume i in ((F /\ G) "" );

      then

      consider w such that

       A1: i = (w " ) and

       A2: w in (F /\ G);

      w in G by A2, XBOOLE_0:def 4;

      then

       A3: (w " ) in (G "" );

      w in F by A2, XBOOLE_0:def 4;

      then (w " ) in (F "" );

      hence thesis by A1, A3, XBOOLE_0:def 4;

    end;

    theorem :: MEMBER_1:25

    ( -- (F "" )) = (( -- F) "" )

    proof

      let i;

      hereby

        assume i in ( -- (F "" ));

        then ( - i) in (F "" ) by Th2;

        then

        consider w such that

         A1: ( - i) = (w " ) and

         A2: w in F;

        (( - w) " ) = ( - (w " )) & ( - w) in ( -- F) by A2, XXREAL_3: 99;

        hence i in (( -- F) "" ) by A1;

      end;

      assume i in (( -- F) "" );

      then

      consider w such that

       A3: i = (w " ) and

       A4: w in ( -- F);

      (( - w) " ) = ( - (w " )) & ( - w) in F by A4, Th2, XXREAL_3: 99;

      then ( - i) in (F "" ) by A3;

      hence thesis by Th2;

    end;

    theorem :: MEMBER_1:26



     Th26: ( {f} "" ) = {(f " )}

    proof

      let i;

      hereby

        assume i in ( {f} "" );

        then

        consider w such that

         A1: i = (w " ) and

         A2: w in {f};

        w = f by A2, TARSKI:def 1;

        hence i in {(f " )} by A1, TARSKI:def 1;

      end;

      assume i in {(f " )};

      then

       A3: i = (f " ) by TARSKI:def 1;

      f in ExtREAL & f in {f} by TARSKI:def 1, XXREAL_0:def 1;

      hence thesis by A3;

    end;

    theorem :: MEMBER_1:27



     Th27: ( {f, g} "" ) = {(f " ), (g " )}

    proof



      thus ( {f, g} "" ) = (( {f} \/ {g}) "" ) by ENUMSET1: 1

      .= (( {f} "" ) \/ ( {g} "" )) by Th23

      .= ( {(f " )} \/ ( {g} "" )) by Th26

      .= ( {(f " )} \/ {(g " )}) by Th26

      .= {(f " ), (g " )} by ENUMSET1: 1;

    end;

    definition

      let A be complex-membered set;

      :: MEMBER_1:def4

      func A "" -> complex-membered set equals { (c " ) : c in A };

      coherence

      proof

        { (c " ) : c in A } is complex-membered

        proof

          let e be object;

          assume e in { (c " ) : c in A };

          then ex c st e = (c " ) & c in A;

          hence thesis;

        end;

        hence thesis;

      end;

      involutiveness

      proof

        let A, B;

        assume

         A1: A = { (c " ) : c in B };

        thus B c= { (c " ) : c in A }

        proof

          let z;



           A2: (z " ) in COMPLEX & z = ((z " ) " ) by XCMPLX_0:def 2;

          assume z in B;

          then (z " ) in A by A1;

          hence thesis by A2;

        end;

        let e be object;

        assume e in { (c " ) : c in A };

        then

        consider r0 be Complex such that

         A3: (r0 " ) = e and

         A4: r0 in A;

        ex c st (c " ) = r0 & c in B by A1, A4;

        hence thesis by A3;

      end;

    end

    theorem :: MEMBER_1:28



     Th28: a in A iff (a " ) in (A "" )

    proof

      thus a in A implies (a " ) in (A "" );

      assume (a " ) in (A "" );

      then ex c st (c " ) = (a " ) & c in A;

      hence thesis by XCMPLX_1: 201;

    end;

    theorem :: MEMBER_1:29



     Th29: (a " ) in A iff a in (A "" )

    proof

      ((a " ) " ) = a;

      hence thesis by Th28;

    end;

    registration

      let A be empty set;

      cluster (A "" ) -> empty;

      coherence

      proof

        assume (A "" ) is non empty;

        then the Element of (A "" ) in (A "" );

        then ex c st the Element of (A "" ) = (c " ) & c in A;

        hence thesis;

      end;

    end

    registration

      let A be complex-membered non empty set;

      cluster (A "" ) -> non empty;

      coherence

      proof

        ( the Element of A " ) in (A "" );

        hence thesis;

      end;

    end

    registration

      let A be real-membered set;

      cluster (A "" ) -> real-membered;

      coherence

      proof

        let e be object;

        assume e in (A "" );

        then ex c st e = (c " ) & c in A;

        hence thesis;

      end;

    end

    registration

      let A be rational-membered set;

      cluster (A "" ) -> rational-membered;

      coherence

      proof

        let e be object;

        assume e in (A "" );

        then ex c st e = (c " ) & c in A;

        hence thesis;

      end;

    end

    registration

      let A be real-membered set, F be ext-real-membered set;

      identify F "" with A "" when A = F;

      compatibility

      proof

        assume

         A1: A = F;

        let a be ExtReal;

        hereby

          assume a in (A "" );

          then

          consider c such that

           A2: a = (c " ) and

           A3: c in A;

          reconsider w = c as Element of ExtREAL by A3, XXREAL_0:def 1;

          ex m be Complex st w = m & (w " ) = (m " ) by A3, XXREAL_3:def 6;

          hence a in (F "" ) by A1, A2, A3;

        end;

        assume a in (F "" );

        then

        consider w such that

         A4: a = (w " ) and

         A5: w in F;

        reconsider c = w as Element of COMPLEX by A1, A5, XCMPLX_0:def 2;

        (w " ) = (c " ) by A1, A5, XXREAL_3:def 6;

        hence thesis by A1, A4, A5;

      end;

    end



     Lm3: A c= B implies (A "" ) c= (B "" )

    proof

      assume

       A1: A c= B;

      let a;

      assume a in (A "" );

      then (a " ) in A by Th29;

      hence thesis by A1, Th29;

    end;

    theorem :: MEMBER_1:30



     Th30: A c= B iff (A "" ) c= (B "" )

    proof

      ((A "" ) "" ) = A & ((B "" ) "" ) = B;

      hence thesis by Lm3;

    end;

    theorem :: MEMBER_1:31

    (A "" ) = (B "" ) implies A = B

    proof

      assume (A "" ) = (B "" );

      then A c= B & B c= A by Th30;

      hence thesis;

    end;

    theorem :: MEMBER_1:32



     Th32: ((A \/ B) "" ) = ((A "" ) \/ (B "" ))

    proof

      let a;

      hereby

        assume a in ((A \/ B) "" );

        then (a " ) in (A \/ B) by Th29;

        then (a " ) in A or (a " ) in B by XBOOLE_0:def 3;

        then a in (A "" ) or a in (B "" ) by Th29;

        hence a in ((A "" ) \/ (B "" )) by XBOOLE_0:def 3;

      end;

      assume a in ((A "" ) \/ (B "" ));

      then a in (A "" ) or a in (B "" ) by XBOOLE_0:def 3;

      then (a " ) in A or (a " ) in B by Th29;

      then (a " ) in (A \/ B) by XBOOLE_0:def 3;

      hence thesis by Th29;

    end;

    theorem :: MEMBER_1:33



     Th33: ((A /\ B) "" ) = ((A "" ) /\ (B "" ))

    proof

      let a;

      hereby

        assume a in ((A /\ B) "" );

        then

         A1: (a " ) in (A /\ B) by Th29;

        then (a " ) in B by XBOOLE_0:def 4;

        then

         A2: a in (B "" ) by Th29;

        (a " ) in A by A1, XBOOLE_0:def 4;

        then a in (A "" ) by Th29;

        hence a in ((A "" ) /\ (B "" )) by A2, XBOOLE_0:def 4;

      end;

      assume

       A3: a in ((A "" ) /\ (B "" ));

      then a in (B "" ) by XBOOLE_0:def 4;

      then

       A4: (a " ) in B by Th29;

      a in (A "" ) by A3, XBOOLE_0:def 4;

      then (a " ) in A by Th29;

      then (a " ) in (A /\ B) by A4, XBOOLE_0:def 4;

      hence thesis by Th29;

    end;

    theorem :: MEMBER_1:34



     Th34: ((A \ B) "" ) = ((A "" ) \ (B "" ))

    proof

      let a;

      hereby

        assume a in ((A \ B) "" );

        then

         A1: (a " ) in (A \ B) by Th29;

        then not (a " ) in B by XBOOLE_0:def 5;

        then

         A2: not a in (B "" ) by Th29;

        a in (A "" ) by A1, Th29;

        hence a in ((A "" ) \ (B "" )) by A2, XBOOLE_0:def 5;

      end;

      assume

       A3: a in ((A "" ) \ (B "" ));

      then not a in (B "" ) by XBOOLE_0:def 5;

      then

       A4: not (a " ) in B by Th29;

      (a " ) in A by A3, Th29;

      then (a " ) in (A \ B) by A4, XBOOLE_0:def 5;

      hence thesis by Th29;

    end;

    theorem :: MEMBER_1:35



     Th35: ((A \+\ B) "" ) = ((A "" ) \+\ (B "" ))

    proof



      thus ((A \+\ B) "" ) = (((A \ B) "" ) \/ ((B \ A) "" )) by Th32

      .= (((A "" ) \ (B "" )) \/ ((B \ A) "" )) by Th34

      .= ((A "" ) \+\ (B "" )) by Th34;

    end;

    theorem :: MEMBER_1:36



     Th36: ( -- (A "" )) = (( -- A) "" )

    proof

      let a;



       A1: (( - a) " ) = ( - (a " )) by XCMPLX_1: 222;

      hereby

        assume a in ( -- (A "" ));

        then ( - a) in (A "" ) by Th12;

        then (( - a) " ) in A by Th29;

        then (a " ) in ( -- A) by A1, Th12;

        hence a in (( -- A) "" ) by Th29;

      end;

      assume a in (( -- A) "" );

      then (a " ) in ( -- A) by Th29;

      then ( - (a " )) in A by Th12;

      then ( - a) in (A "" ) by A1, Th29;

      hence thesis by Th12;

    end;

    theorem :: MEMBER_1:37



     Th37: ( {a} "" ) = {(a " )}

    proof

      let z;

      hereby

        assume z in ( {a} "" );

        then

        consider c such that

         A1: z = (c " ) and

         A2: c in {a};

        c = a by A2, TARSKI:def 1;

        hence z in {(a " )} by A1, TARSKI:def 1;

      end;

      assume z in {(a " )};

      then

       A3: z = (a " ) by TARSKI:def 1;

      a in COMPLEX & a in {a} by TARSKI:def 1, XCMPLX_0:def 2;

      hence thesis by A3;

    end;

    theorem :: MEMBER_1:38



     Th38: ( {a, b} "" ) = {(a " ), (b " )}

    proof

      let z;

      hereby

        assume z in ( {a, b} "" );

        then

        consider c such that

         A1: z = (c " ) and

         A2: c in {a, b};

        c = a or c = b by A2, TARSKI:def 2;

        hence z in {(a " ), (b " )} by A1, TARSKI:def 2;

      end;



       A3: a in {a, b} & b in {a, b} by TARSKI:def 2;

      assume z in {(a " ), (b " )};

      then

       A4: z = (a " ) or z = (b " ) by TARSKI:def 2;

      thus thesis by A4, A3;

    end;

    definition

      let F,G be ext-real-membered set;

      :: MEMBER_1:def5

      func F ++ G -> set equals { (w1 + w2) : w1 in F & w2 in G };

      coherence ;

      commutativity

      proof

        let X be set;

        let F, G;

        assume

         A1: X = { (w1 + w2) : w1 in F & w2 in G };

        thus X c= { (w1 + w2) : w1 in G & w2 in F }

        proof

          let e be object;

          assume e in X;

          then ex w1, w2 st e = (w1 + w2) & w1 in F & w2 in G by A1;

          hence thesis;

        end;

        let e be object;

        assume e in { (w1 + w2) : w1 in G & w2 in F };

        then ex w1, w2 st e = (w1 + w2) & w1 in G & w2 in F;

        hence thesis by A1;

      end;

    end

    theorem :: MEMBER_1:39



     Th39: f in F & g in G implies (f + g) in (F ++ G)

    proof

      f in ExtREAL & g in ExtREAL by XXREAL_0:def 1;

      hence thesis;

    end;

    registration

      let F be empty set;

      let G be ext-real-membered set;

      cluster (F ++ G) -> empty;

      coherence

      proof

        assume (F ++ G) is non empty;

        then the Element of (F ++ G) in (F ++ G);

        then ex w1, w2 st the Element of (F ++ G) = (w1 + w2) & w1 in F & w2 in G;

        hence thesis;

      end;

      cluster (G ++ F) -> empty;

      coherence ;

    end

    registration

      let F,G be ext-real-membered non empty set;

      cluster (F ++ G) -> non empty;

      coherence

      proof

        ( the Element of F + the Element of G) in (F ++ G) by Th39;

        hence thesis;

      end;

    end

    registration

      let F,G be ext-real-membered set;

      cluster (F ++ G) -> ext-real-membered;

      coherence

      proof

        let e be object;

        assume e in (F ++ G);

        then ex w1, w2 st e = (w1 + w2) & w1 in F & w2 in G;

        hence thesis;

      end;

    end

    theorem :: MEMBER_1:40

    F c= G & H c= I implies (F ++ H) c= (G ++ I)

    proof

      assume

       A1: F c= G & H c= I;

      let i;

      assume i in (F ++ H);

      then ex w, w1 st i = (w + w1) & w in F & w1 in H;

      hence thesis by A1;

    end;

    theorem :: MEMBER_1:41



     Th41: (F ++ (G \/ H)) = ((F ++ G) \/ (F ++ H))

    proof

      let j;

      hereby

        assume j in (F ++ (G \/ H));

        then

        consider w, w1 such that

         A1: j = (w + w1) and

         A2: w in F and

         A3: w1 in (G \/ H);

        w1 in G or w1 in H by A3, XBOOLE_0:def 3;

        then (w + w1) in (F ++ G) or (w + w1) in (F ++ H) by A2;

        hence j in ((F ++ G) \/ (F ++ H)) by A1, XBOOLE_0:def 3;

      end;

      assume

       A4: j in ((F ++ G) \/ (F ++ H));

      per cases by A4, XBOOLE_0:def 3;

        suppose j in (F ++ G);

        then

        consider w, w1 such that

         A5: j = (w + w1) & w in F and

         A6: w1 in G;

        w1 in (G \/ H) by A6, XBOOLE_0:def 3;

        hence thesis by A5;

      end;

        suppose j in (F ++ H);

        then

        consider w, w1 such that

         A7: j = (w + w1) & w in F and

         A8: w1 in H;

        w1 in (G \/ H) by A8, XBOOLE_0:def 3;

        hence thesis by A7;

      end;

    end;

    theorem :: MEMBER_1:42



     Th42: (F ++ (G /\ H)) c= ((F ++ G) /\ (F ++ H))

    proof

      let j;

      assume j in (F ++ (G /\ H));

      then

      consider w, w1 such that

       A1: j = (w + w1) and

       A2: w in F and

       A3: w1 in (G /\ H);

      w1 in H by A3, XBOOLE_0:def 4;

      then

       A4: (w + w1) in (F ++ H) by A2;

      w1 in G by A3, XBOOLE_0:def 4;

      then (w + w1) in (F ++ G) by A2;

      hence thesis by A1, A4, XBOOLE_0:def 4;

    end;

    theorem :: MEMBER_1:43



     Th43: ( {f} ++ {g}) = {(f + g)}

    proof

      let j;

      hereby

        assume j in ( {f} ++ {g});

        then

        consider w1, w2 such that

         A1: j = (w1 + w2) and

         A2: w1 in {f} & w2 in {g};

        w1 = f & w2 = g by A2, TARSKI:def 1;

        hence j in {(f + g)} by A1, TARSKI:def 1;

      end;



       A3: f in {f} & g in {g} by TARSKI:def 1;

      assume j in {(f + g)};

      then

       A4: j = (f + g) by TARSKI:def 1;

      f in ExtREAL & g in ExtREAL by XXREAL_0:def 1;

      hence thesis by A4, A3;

    end;

    theorem :: MEMBER_1:44



     Th44: ( {f} ++ {g, h}) = {(f + g), (f + h)}

    proof



      thus ( {f} ++ {g, h}) = ( {f} ++ ( {g} \/ {h})) by ENUMSET1: 1

      .= (( {f} ++ {g}) \/ ( {f} ++ {h})) by Th41

      .= ( {(f + g)} \/ ( {f} ++ {h})) by Th43

      .= ( {(f + g)} \/ {(f + h)}) by Th43

      .= {(f + g), (f + h)} by ENUMSET1: 1;

    end;

    theorem :: MEMBER_1:45



     Th45: ( {f, g} ++ {h, i}) = {(f + h), (f + i), (g + h), (g + i)}

    proof



      thus ( {f, g} ++ {h, i}) = (( {f} \/ {g}) ++ {h, i}) by ENUMSET1: 1

      .= (( {f} ++ {h, i}) \/ ( {g} ++ {h, i})) by Th41

      .= ( {(f + h), (f + i)} \/ ( {g} ++ {h, i})) by Th44

      .= ( {(f + h), (f + i)} \/ {(g + h), (g + i)}) by Th44

      .= {(f + h), (f + i), (g + h), (g + i)} by ENUMSET1: 5;

    end;

    definition

      let A,B be complex-membered set;

      :: MEMBER_1:def6

      func A ++ B -> set equals { (c1 + c2) : c1 in A & c2 in B };

      coherence ;

      commutativity

      proof

        let X be set;

        let A, B;

        assume

         A1: X = { (c1 + c2) : c1 in A & c2 in B };

        thus X c= { (c1 + c2) : c1 in B & c2 in A }

        proof

          let e be object;

          assume e in X;

          then ex c1, c2 st e = (c1 + c2) & c1 in A & c2 in B by A1;

          hence thesis;

        end;

        let e be object;

        assume e in { (c1 + c2) : c1 in B & c2 in A };

        then ex c1, c2 st e = (c1 + c2) & c1 in B & c2 in A;

        hence thesis by A1;

      end;

    end

    theorem :: MEMBER_1:46

    a in A & b in B implies (a + b) in (A ++ B);

    registration

      let A be empty set;

      let B be complex-membered set;

      cluster (A ++ B) -> empty;

      coherence

      proof

        assume (A ++ B) is non empty;

        then the Element of (A ++ B) in (A ++ B);

        then ex c1, c2 st the Element of (A ++ B) = (c1 + c2) & c1 in A & c2 in B;

        hence thesis;

      end;

      cluster (B ++ A) -> empty;

      coherence ;

    end

    registration

      let A,B be complex-membered non empty set;

      cluster (A ++ B) -> non empty;

      coherence

      proof

        ( the Element of A + the Element of B) in (A ++ B);

        hence thesis;

      end;

    end

    registration

      let A,B be complex-membered set;

      cluster (A ++ B) -> complex-membered;

      coherence

      proof

        let e be object;

        assume e in (A ++ B);

        then ex c1, c2 st e = (c1 + c2) & c1 in A & c2 in B;

        hence thesis;

      end;

    end

    registration

      let A,B be real-membered set;

      cluster (A ++ B) -> real-membered;

      coherence

      proof

        let e be object;

        assume e in (A ++ B);

        then ex c1, c2 st e = (c1 + c2) & c1 in A & c2 in B;

        hence thesis;

      end;

    end

    registration

      let A,B be rational-membered set;

      cluster (A ++ B) -> rational-membered;

      coherence

      proof

        let e be object;

        assume e in (A ++ B);

        then ex c1, c2 st e = (c1 + c2) & c1 in A & c2 in B;

        hence thesis;

      end;

    end

    registration

      let A,B be integer-membered set;

      cluster (A ++ B) -> integer-membered;

      coherence

      proof

        let e be object;

        assume e in (A ++ B);

        then ex c1, c2 st e = (c1 + c2) & c1 in A & c2 in B;

        hence thesis;

      end;

    end

    registration

      let A,B be natural-membered set;

      cluster (A ++ B) -> natural-membered;

      coherence

      proof

        let e be object;

        assume e in (A ++ B);

        then ex c1, c2 st e = (c1 + c2) & c1 in A & c2 in B;

        hence thesis;

      end;

    end

    registration

      let A,B be real-membered set, F,G be ext-real-membered set;

      identify F ++ G with A ++ B when A = F, B = G;

      compatibility

      proof

        assume

         A1: A = F & B = G;

        let a be ExtReal;

        hereby

          assume a in (A ++ B);

          then

          consider c, c1 such that

           A2: a = (c + c1) and

           A3: c in A & c1 in B;

          reconsider d1 = c, d2 = c1 as Element of ExtREAL by A3, XXREAL_0:def 1;

          a = (d1 + d2) by A2, A3, XXREAL_3:def 2;

          hence a in (F ++ G) by A1, A3;

        end;

        assume a in (F ++ G);

        then

        consider w, w1 such that

         A4: a = (w + w1) and

         A5: w in F & w1 in G;

        reconsider d1 = w, d2 = w1 as Element of COMPLEX by A1, A5, XCMPLX_0:def 2;

        a = (d1 + d2) by A1, A4, A5, XXREAL_3:def 2;

        hence thesis by A1, A5;

      end;

    end

    theorem :: MEMBER_1:47



     Th47: A c= B & C c= D implies (A ++ C) c= (B ++ D)

    proof

      assume

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

      let a;

      assume a in (A ++ C);

      then ex c, c1 st a = (c + c1) & c in A & c1 in C;

      hence thesis by A1;

    end;

    theorem :: MEMBER_1:48



     Th48: (A ++ (B \/ C)) = ((A ++ B) \/ (A ++ C))

    proof

      let a;

      hereby

        assume a in (A ++ (B \/ C));

        then

        consider c, c1 such that

         A1: a = (c + c1) and

         A2: c in A and

         A3: c1 in (B \/ C);

        c1 in B or c1 in C by A3, XBOOLE_0:def 3;

        then (c + c1) in (A ++ B) or (c + c1) in (A ++ C) by A2;

        hence a in ((A ++ B) \/ (A ++ C)) by A1, XBOOLE_0:def 3;

      end;

      assume

       A4: a in ((A ++ B) \/ (A ++ C));

      per cases by A4, XBOOLE_0:def 3;

        suppose a in (A ++ B);

        then

        consider c, c1 such that

         A5: a = (c + c1) & c in A and

         A6: c1 in B;

        c1 in (B \/ C) by A6, XBOOLE_0:def 3;

        hence thesis by A5;

      end;

        suppose a in (A ++ C);

        then

        consider c, c1 such that

         A7: a = (c + c1) & c in A and

         A8: c1 in C;

        c1 in (B \/ C) by A8, XBOOLE_0:def 3;

        hence thesis by A7;

      end;

    end;

    theorem :: MEMBER_1:49



     Th49: (A ++ (B /\ C)) c= ((A ++ B) /\ (A ++ C))

    proof

      let a;

      assume a in (A ++ (B /\ C));

      then

      consider c, c1 such that

       A1: a = (c + c1) and

       A2: c in A and

       A3: c1 in (B /\ C);

      c1 in C by A3, XBOOLE_0:def 4;

      then

       A4: (c + c1) in (A ++ C) by A2;

      c1 in B by A3, XBOOLE_0:def 4;

      then (c + c1) in (A ++ B) by A2;

      hence thesis by A1, A4, XBOOLE_0:def 4;

    end;

    theorem :: MEMBER_1:50



     Th50: ((A ++ B) ++ C) = (A ++ (B ++ C))

    proof

      let a;

      hereby

        assume a in ((A ++ B) ++ C);

        then

        consider c, c1 such that

         A1: a = (c + c1) and

         A2: c in (A ++ B) and

         A3: c1 in C;

        consider c2,c3 be Complex such that

         A4: c = (c2 + c3) and

         A5: c2 in A and

         A6: c3 in B by A2;

        a = (c2 + (c3 + c1)) & (c3 + c1) in (B ++ C) by A1, A3, A4, A6;

        hence a in (A ++ (B ++ C)) by A5;

      end;

      assume a in (A ++ (B ++ C));

      then

      consider c, c1 such that

       A7: a = (c + c1) & c in A and

       A8: c1 in (B ++ C);

      consider c2,c3 be Complex such that

       A9: c1 = (c2 + c3) & c2 in B and

       A10: c3 in C by A8;

      a = ((c + c2) + c3) & (c + c2) in (A ++ B) by A7, A9;

      hence thesis by A10;

    end;

    theorem :: MEMBER_1:51



     Th51: ( {a} ++ {b}) = {(a + b)}

    proof

      let z;

      hereby

        assume z in ( {a} ++ {b});

        then

        consider c1, c2 such that

         A1: z = (c1 + c2) and

         A2: c1 in {a} & c2 in {b};

        c1 = a & c2 = b by A2, TARSKI:def 1;

        hence z in {(a + b)} by A1, TARSKI:def 1;

      end;



       A3: a in {a} & b in {b} by TARSKI:def 1;

      assume z in {(a + b)};

      then

       A4: z = (a + b) by TARSKI:def 1;

      thus thesis by A4, A3;

    end;

    theorem :: MEMBER_1:52



     Th52: ( {a} ++ {s, t}) = {(a + s), (a + t)}

    proof



      thus ( {a} ++ {s, t}) = ( {a} ++ ( {s} \/ {t})) by ENUMSET1: 1

      .= (( {a} ++ {s}) \/ ( {a} ++ {t})) by Th48

      .= ( {(a + s)} \/ ( {a} ++ {t})) by Th51

      .= ( {(a + s)} \/ {(a + t)}) by Th51

      .= {(a + s), (a + t)} by ENUMSET1: 1;

    end;

    theorem :: MEMBER_1:53



     Th53: ( {a, b} ++ {s, t}) = {(a + s), (a + t), (b + s), (b + t)}

    proof



      thus ( {a, b} ++ {s, t}) = (( {a} \/ {b}) ++ {s, t}) by ENUMSET1: 1

      .= (( {a} ++ {s, t}) \/ ( {b} ++ {s, t})) by Th48

      .= ( {(a + s), (a + t)} \/ ( {b} ++ {s, t})) by Th52

      .= ( {(a + s), (a + t)} \/ {(b + s), (b + t)}) by Th52

      .= {(a + s), (a + t), (b + s), (b + t)} by ENUMSET1: 5;

    end;

    definition

      let F,G be ext-real-membered set;

      :: MEMBER_1:def7

      func F -- G -> set equals (F ++ ( -- G));

      coherence ;

    end

    theorem :: MEMBER_1:54



     Th54: (F -- G) = { (w1 - w2) : w1 in F & w2 in G }

    proof

      thus (F -- G) c= { (w1 - w2) : w1 in F & w2 in G }

      proof

        let e be object;

        assume e in (F -- G);

        then

        consider w1, w2 such that

         A1: e = (w1 + w2) and

         A2: w1 in F and

         A3: w2 in ( -- G);

        e = (w1 - ( - w2)) & ( - w2) in G by A1, A3, Th2;

        hence thesis by A2;

      end;

      let e be object;

      assume e in { (w1 - w2) : w1 in F & w2 in G };

      then

      consider w1, w2 such that

       A4: e = (w1 - w2) & w1 in F and

       A5: w2 in G;

      ( - w2) in ( -- G) by A5;

      hence thesis by A4;

    end;

    theorem :: MEMBER_1:55



     Th55: f in F & g in G implies (f - g) in (F -- G)

    proof



       A1: f in ExtREAL & g in ExtREAL by XXREAL_0:def 1;

      (F -- G) = { (w1 - w2) : w1 in F & w2 in G } by Th54;

      hence thesis by A1;

    end;

    registration

      let F be empty set;

      let G be ext-real-membered set;

      cluster (F -- G) -> empty;

      coherence ;

      cluster (G -- F) -> empty;

      coherence ;

    end

    registration

      let F,G be ext-real-membered non empty set;

      cluster (F -- G) -> non empty;

      coherence ;

    end

    registration

      let F,G be ext-real-membered set;

      cluster (F -- G) -> ext-real-membered;

      coherence ;

    end

    theorem :: MEMBER_1:56

    F c= G & H c= I implies (F -- H) c= (G -- I)

    proof

      assume

       A1: F c= G & H c= I;

      let i;



       A2: (F -- H) = { (w1 - w2) : w1 in F & w2 in H } by Th54;

      assume i in (F -- H);

      then ex w, w1 st i = (w - w1) & w in F & w1 in H by A2;

      hence thesis by A1, Th55;

    end;

    theorem :: MEMBER_1:57

    (F -- (G \/ H)) = ((F -- G) \/ (F -- H))

    proof



      thus (F -- (G \/ H)) = (F ++ (( -- G) \/ ( -- H))) by Th5

      .= ((F -- G) \/ (F -- H)) by Th41;

    end;

    theorem :: MEMBER_1:58

    (F -- (G /\ H)) c= ((F -- G) /\ (F -- H))

    proof

      (F -- (G /\ H)) = (F ++ (( -- G) /\ ( -- H))) by Th6;

      hence thesis by Th42;

    end;



     Lm4: ( -- (F ++ G)) = (( -- F) ++ ( -- G))

    proof

      let j;

      hereby

        assume j in ( -- (F ++ G));

        then

        consider w such that

         A1: j = ( - w) and

         A2: w in (F ++ G);

        consider w1, w2 such that

         A3: w = (w1 + w2) and

         A4: w1 in F & w2 in G by A2;



         A5: ( - (w1 + w2)) = (( - w1) - w2) by XXREAL_3: 9;

        ( - w1) in ( -- F) & ( - w2) in ( -- G) by A4;

        hence j in (( -- F) ++ ( -- G)) by A1, A3, A5;

      end;

      assume j in (( -- F) ++ ( -- G));

      then

      consider w1, w2 such that

       A6: j = (w1 + w2) and

       A7: w1 in ( -- F) & w2 in ( -- G);

      ( - w1) in F & ( - w2) in G by A7, Th2;

      then ( - (w1 + w2)) = (( - w1) - w2) & (( - w1) + ( - w2)) in (F ++ G) by XXREAL_3: 9;

      hence thesis by A6, Th2;

    end;

    theorem :: MEMBER_1:59

    ( -- (F ++ G)) = (( -- F) -- G) by Lm4;

    theorem :: MEMBER_1:60



     Th60: ( -- (F -- G)) = (( -- F) ++ G)

    proof



      thus ( -- (F -- G)) = (( -- F) -- ( -- G)) by Lm4

      .= (( -- F) ++ G);

    end;

    theorem :: MEMBER_1:61

    ( {f} -- {g}) = {(f - g)}

    proof



      thus ( {f} -- {g}) = ( {f} ++ {( - g)}) by Th9

      .= {(f - g)} by Th43;

    end;

    theorem :: MEMBER_1:62

    ( {f} -- {h, i}) = {(f - h), (f - i)}

    proof



      thus ( {f} -- {h, i}) = ( {f} ++ {( - h), ( - i)}) by Th10

      .= {(f - h), (f - i)} by Th44;

    end;

    theorem :: MEMBER_1:63

    ( {f, g} -- {h}) = {(f - h), (g - h)}

    proof



      thus ( {f, g} -- {h}) = ( {f, g} ++ {( - h)}) by Th9

      .= {(f - h), (g - h)} by Th44;

    end;

    theorem :: MEMBER_1:64

    ( {f, g} -- {h, i}) = {(f - h), (f - i), (g - h), (g - i)}

    proof



      thus ( {f, g} -- {h, i}) = ( {f, g} ++ {( - h), ( - i)}) by Th10

      .= {(f - h), (f - i), (g - h), (g - i)} by Th45;

    end;

    definition

      let A,B be complex-membered set;

      :: MEMBER_1:def8

      func A -- B -> set equals (A ++ ( -- B));

      coherence ;

    end

    theorem :: MEMBER_1:65



     Th65: (A -- B) = { (c1 - c2) : c1 in A & c2 in B }

    proof

      thus (A -- B) c= { (c1 - c2) : c1 in A & c2 in B }

      proof

        let e be object;

        assume e in (A -- B);

        then

        consider c1, c2 such that

         A1: e = (c1 + c2) and

         A2: c1 in A and

         A3: c2 in ( -- B);

        e = (c1 - ( - c2)) & ( - c2) in B by A1, A3, Th12;

        hence thesis by A2;

      end;

      let e be object;

      assume e in { (c1 - c2) : c1 in A & c2 in B };

      then

      consider c1, c2 such that

       A4: e = (c1 - c2) & c1 in A and

       A5: c2 in B;

      ( - c2) in ( -- B) by A5;

      hence thesis by A4;

    end;

    theorem :: MEMBER_1:66



     Th66: a in A & b in B implies (a - b) in (A -- B)

    proof

      (A -- B) = { (c1 - c2) : c1 in A & c2 in B } by Th65;

      hence thesis;

    end;

    registration

      let A be empty set;

      let B be complex-membered set;

      cluster (A -- B) -> empty;

      coherence ;

      cluster (B -- A) -> empty;

      coherence ;

    end

    registration

      let A,B be complex-membered non empty set;

      cluster (A -- B) -> non empty;

      coherence ;

    end

    registration

      let A,B be complex-membered set;

      cluster (A -- B) -> complex-membered;

      coherence ;

    end

    registration

      let A,B be real-membered set;

      cluster (A -- B) -> real-membered;

      coherence ;

    end

    registration

      let A,B be rational-membered set;

      cluster (A -- B) -> rational-membered;

      coherence ;

    end

    registration

      let A,B be integer-membered set;

      cluster (A -- B) -> integer-membered;

      coherence ;

    end

    registration

      let A,B be real-membered set, F,G be ext-real-membered set;

      identify F -- G with A -- B when A = F, B = G;

      compatibility ;

    end

    theorem :: MEMBER_1:67



     Th67: A c= B & C c= D implies (A -- C) c= (B -- D)

    proof

      assume

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

      let z;



       A2: (A -- C) = { (c1 - c2) : c1 in A & c2 in C } by Th65;

      assume z in (A -- C);

      then ex c, c1 st z = (c - c1) & c in A & c1 in C by A2;

      hence thesis by A1, Th66;

    end;



     Lm5: ( -- (A ++ B)) = (( -- A) ++ ( -- B))

    proof

      let a;

      hereby

        assume a in ( -- (A ++ B));

        then

        consider c such that

         A1: a = ( - c) and

         A2: c in (A ++ B);

        consider c1, c2 such that

         A3: c = (c1 + c2) and

         A4: c1 in A & c2 in B by A2;



         A5: ( - c1) in ( -- A) & ( - c2) in ( -- B) by A4;

        a = (( - c1) + ( - c2)) by A1, A3;

        hence a in (( -- A) ++ ( -- B)) by A5;

      end;

      assume a in (( -- A) ++ ( -- B));

      then

      consider c1, c2 such that

       A6: a = (c1 + c2) and

       A7: c1 in ( -- A) & c2 in ( -- B);

      ( - c1) in A & ( - c2) in B by A7, Th12;

      then (( - c1) + ( - c2)) in (A ++ B);

      then ( - a) in (A ++ B) by A6;

      hence thesis by Th12;

    end;

    theorem :: MEMBER_1:68

    (A -- (B \/ C)) = ((A -- B) \/ (A -- C))

    proof



      thus (A -- (B \/ C)) = (A ++ (( -- B) \/ ( -- C))) by Th15

      .= ((A -- B) \/ (A -- C)) by Th48;

    end;

    theorem :: MEMBER_1:69

    (A -- (B /\ C)) c= ((A -- B) /\ (A -- C))

    proof

      (A -- (B /\ C)) = (A ++ (( -- B) /\ ( -- C))) by Th16;

      hence thesis by Th49;

    end;

    theorem :: MEMBER_1:70

    ( -- (A ++ B)) = (( -- A) -- B) by Lm5;

    theorem :: MEMBER_1:71



     Th71: ( -- (A -- B)) = (( -- A) ++ B)

    proof



      thus ( -- (A -- B)) = (( -- A) -- ( -- B)) by Lm5

      .= (( -- A) ++ B);

    end;

    theorem :: MEMBER_1:72

    (A ++ (B -- C)) = ((A ++ B) -- C) by Th50;

    theorem :: MEMBER_1:73

    (A -- (B ++ C)) = ((A -- B) -- C)

    proof



      thus (A -- (B ++ C)) = (A ++ (( -- B) -- C)) by Lm5

      .= ((A -- B) -- C) by Th50;

    end;

    theorem :: MEMBER_1:74

    (A -- (B -- C)) = ((A -- B) ++ C)

    proof



      thus (A -- (B -- C)) = (A ++ (( -- B) ++ C)) by Th71

      .= ((A -- B) ++ C) by Th50;

    end;

    theorem :: MEMBER_1:75



     Th75: ( {a} -- {b}) = {(a - b)}

    proof



      thus ( {a} -- {b}) = ( {a} ++ {( - b)}) by Th19

      .= {(a - b)} by Th51;

    end;

    theorem :: MEMBER_1:76

    ( {a} -- {s, t}) = {(a - s), (a - t)}

    proof



      thus ( {a} -- {s, t}) = ( {a} ++ {( - s), ( - t)}) by Th20

      .= {(a - s), (a - t)} by Th52;

    end;

    theorem :: MEMBER_1:77

    ( {a, b} -- {s}) = {(a - s), (b - s)}

    proof



      thus ( {a, b} -- {s}) = ( {a, b} ++ {( - s)}) by Th19

      .= {(a - s), (b - s)} by Th52;

    end;

    theorem :: MEMBER_1:78

    ( {a, b} -- {s, t}) = {(a - s), (a - t), (b - s), (b - t)}

    proof



      thus ( {a, b} -- {s, t}) = ( {a, b} ++ {( - s), ( - t)}) by Th20

      .= {(a - s), (a - t), (b - s), (b - t)} by Th53;

    end;

    definition

      let F,G be ext-real-membered set;

      :: MEMBER_1:def9

      func F ** G -> set equals { (w1 * w2) : w1 in F & w2 in G };

      coherence ;

      commutativity

      proof

        let X be set;

        let F, G;

        assume

         A1: X = { (w1 * w2) : w1 in F & w2 in G };

        thus X c= { (w1 * w2) : w1 in G & w2 in F }

        proof

          let e be object;

          assume e in X;

          then ex w1, w2 st e = (w1 * w2) & w1 in F & w2 in G by A1;

          hence thesis;

        end;

        let e be object;

        assume e in { (w1 * w2) : w1 in G & w2 in F };

        then ex w1, w2 st e = (w1 * w2) & w1 in G & w2 in F;

        hence thesis by A1;

      end;

    end

    registration

      let F be empty set;

      let G be ext-real-membered set;

      cluster (F ** G) -> empty;

      coherence

      proof

        assume (F ** G) is non empty;

        then the Element of (F ** G) in (F ** G);

        then ex w1, w2 st the Element of (F ** G) = (w1 * w2) & w1 in F & w2 in G;

        hence thesis;

      end;

      cluster (G ** F) -> empty;

      coherence ;

    end

    registration

      let F,G be ext-real-membered set;

      cluster (F ** G) -> ext-real-membered;

      coherence

      proof

        let e be object;

        assume e in (F ** G);

        then ex w1, w2 st e = (w1 * w2) & w1 in F & w2 in G;

        hence thesis;

      end;

    end

    theorem :: MEMBER_1:79



     Th79: f in F & g in G implies (f * g) in (F ** G)

    proof

      f in ExtREAL & g in ExtREAL by XXREAL_0:def 1;

      hence thesis;

    end;

    registration

      let F,G be ext-real-membered non empty set;

      cluster (F ** G) -> non empty;

      coherence

      proof

        ( the Element of F * the Element of G) in (F ** G) by Th79;

        hence thesis;

      end;

    end

    theorem :: MEMBER_1:80



     Th80: ((F ** G) ** H) = (F ** (G ** H))

    proof

      let i;

      hereby

        assume i in ((F ** G) ** H);

        then

        consider w, w1 such that

         A1: i = (w * w1) and

         A2: w in (F ** G) and

         A3: w1 in H;

        consider w2,w3 be Element of ExtREAL such that

         A4: w = (w2 * w3) and

         A5: w2 in F and

         A6: w3 in G by A2;

        i = (w2 * (w3 * w1)) & (w3 * w1) in (G ** H) by A1, A3, A4, A6, XXREAL_3: 66;

        hence i in (F ** (G ** H)) by A5;

      end;

      assume i in (F ** (G ** H));

      then

      consider w, w1 such that

       A7: i = (w * w1) & w in F and

       A8: w1 in (G ** H);

      consider w2,w3 be Element of ExtREAL such that

       A9: w1 = (w2 * w3) & w2 in G and

       A10: w3 in H by A8;

      i = ((w * w2) * w3) & (w * w2) in (F ** G) by A7, A9, XXREAL_3: 66;

      hence thesis by A10;

    end;

    theorem :: MEMBER_1:81



     Th81: F c= G & H c= I implies (F ** H) c= (G ** I)

    proof

      assume

       A1: F c= G & H c= I;

      let i;

      assume i in (F ** H);

      then ex w, w1 st i = (w * w1) & w in F & w1 in H;

      hence thesis by A1;

    end;

    theorem :: MEMBER_1:82



     Th82: (F ** (G \/ H)) = ((F ** G) \/ (F ** H))

    proof

      let j;

      hereby

        assume j in (F ** (G \/ H));

        then

        consider w, w1 such that

         A1: j = (w * w1) and

         A2: w in F and

         A3: w1 in (G \/ H);

        w1 in G or w1 in H by A3, XBOOLE_0:def 3;

        then (w * w1) in (F ** G) or (w * w1) in (F ** H) by A2;

        hence j in ((F ** G) \/ (F ** H)) by A1, XBOOLE_0:def 3;

      end;

      assume

       A4: j in ((F ** G) \/ (F ** H));

      per cases by A4, XBOOLE_0:def 3;

        suppose j in (F ** G);

        then

        consider w, w1 such that

         A5: j = (w * w1) & w in F and

         A6: w1 in G;

        w1 in (G \/ H) by A6, XBOOLE_0:def 3;

        hence thesis by A5;

      end;

        suppose j in (F ** H);

        then

        consider w, w1 such that

         A7: j = (w * w1) & w in F and

         A8: w1 in H;

        w1 in (G \/ H) by A8, XBOOLE_0:def 3;

        hence thesis by A7;

      end;

    end;

    theorem :: MEMBER_1:83



     Th83: (F ** (G /\ H)) c= ((F ** G) /\ (F ** H))

    proof

      let j;

      assume j in (F ** (G /\ H));

      then

      consider w, w1 such that

       A1: j = (w * w1) and

       A2: w in F and

       A3: w1 in (G /\ H);

      w1 in H by A3, XBOOLE_0:def 4;

      then

       A4: (w * w1) in (F ** H) by A2;

      w1 in G by A3, XBOOLE_0:def 4;

      then (w * w1) in (F ** G) by A2;

      hence thesis by A1, A4, XBOOLE_0:def 4;

    end;

    theorem :: MEMBER_1:84

    (F ** ( -- G)) = ( -- (F ** G))

    proof

      let i;

      hereby

        assume i in (F ** ( -- G));

        then

        consider w, w1 such that

         A1: i = (w * w1) and

         A2: w in F and

         A3: w1 in ( -- G);

        (w * ( - w1)) = ( - (w * w1)) by XXREAL_3: 92;

        then

         A4: i = ( - (w * ( - w1))) by A1;

        ( - w1) in G by A3, Th2;

        then (w * ( - w1)) in (F ** G) by A2;

        hence i in ( -- (F ** G)) by A4;

      end;

      assume i in ( -- (F ** G));

      then ( - i) in (F ** G) by Th2;

      then

      consider w, w1 such that

       A5: ( - i) = (w * w1) & w in F and

       A6: w1 in G;

      (w * ( - w1)) = ( - (w * w1)) & ( - w1) in ( -- G) by A6, XXREAL_3: 92;

      hence thesis by A5;

    end;

    theorem :: MEMBER_1:85



     Th85: ((F ** G) "" ) = ((F "" ) ** (G "" ))

    proof

      let i;

      hereby

        assume i in ((F ** G) "" );

        then

        consider w such that

         A1: i = (w " ) and

         A2: w in (F ** G);

        consider w1, w2 such that

         A3: w = (w1 * w2) and

         A4: w1 in F & w2 in G by A2;



         A5: (w1 " ) in (F "" ) & (w2 " ) in (G "" ) by A4;

        i = ((w1 " ) * (w2 " )) by A1, A3, XXREAL_3: 67;

        hence i in ((F "" ) ** (G "" )) by A5;

      end;

      assume i in ((F "" ) ** (G "" ));

      then

      consider w, w1 such that

       A6: i = (w * w1) and

       A7: w in (F "" ) and

       A8: w1 in (G "" );

      consider w3 be Element of ExtREAL such that

       A9: w1 = (w3 " ) and

       A10: w3 in G by A8;

      consider w2 such that

       A11: w = (w2 " ) and

       A12: w2 in F by A7;



       A13: (w2 * w3) in (F ** G) by A12, A10;

      i = ((w2 * w3) " ) by A6, A11, A9, XXREAL_3: 67;

      hence thesis by A13;

    end;

    theorem :: MEMBER_1:86



     Th86: ( {f} ** {g}) = {(f * g)}

    proof

      let i;

      hereby

        assume i in ( {f} ** {g});

        then

        consider w1, w2 such that

         A1: i = (w1 * w2) and

         A2: w1 in {f} & w2 in {g};

        w1 = f & w2 = g by A2, TARSKI:def 1;

        hence i in {(f * g)} by A1, TARSKI:def 1;

      end;



       A3: f in {f} & g in {g} by TARSKI:def 1;

      assume i in {(f * g)};

      then

       A4: i = (f * g) by TARSKI:def 1;

      f in ExtREAL & g in ExtREAL by XXREAL_0:def 1;

      hence thesis by A4, A3;

    end;

    theorem :: MEMBER_1:87



     Th87: ( {f} ** {h, i}) = {(f * h), (f * i)}

    proof



      thus ( {f} ** {h, i}) = ( {f} ** ( {h} \/ {i})) by ENUMSET1: 1

      .= (( {f} ** {h}) \/ ( {f} ** {i})) by Th82

      .= ( {(f * h)} \/ ( {f} ** {i})) by Th86

      .= ( {(f * h)} \/ {(f * i)}) by Th86

      .= {(f * h), (f * i)} by ENUMSET1: 1;

    end;

    theorem :: MEMBER_1:88



     Th88: ( {f, g} ** {h, i}) = {(f * h), (f * i), (g * h), (g * i)}

    proof



      thus ( {f, g} ** {h, i}) = (( {f} \/ {g}) ** {h, i}) by ENUMSET1: 1

      .= (( {f} ** {h, i}) \/ ( {g} ** {h, i})) by Th82

      .= ( {(f * h), (f * i)} \/ ( {g} ** {h, i})) by Th87

      .= ( {(f * h), (f * i)} \/ {(g * h), (g * i)}) by Th87

      .= {(f * h), (f * i), (g * h), (g * i)} by ENUMSET1: 5;

    end;

    definition

      let A,B be complex-membered set;

      :: MEMBER_1:def10

      func A ** B -> set equals { (c1 * c2) : c1 in A & c2 in B };

      coherence ;

      commutativity

      proof

        let X be set;

        let A, B;

        assume

         A1: X = { (c1 * c2) : c1 in A & c2 in B };

        thus X c= { (c1 * c2) : c1 in B & c2 in A }

        proof

          let e be object;

          assume e in X;

          then ex c1, c2 st e = (c1 * c2) & c1 in A & c2 in B by A1;

          hence thesis;

        end;

        let e be object;

        assume e in { (c1 * c2) : c1 in B & c2 in A };

        then ex c1, c2 st e = (c1 * c2) & c1 in B & c2 in A;

        hence thesis by A1;

      end;

    end

    theorem :: MEMBER_1:89

    a in A & b in B implies (a * b) in (A ** B);

    registration

      let A be empty set;

      let B be complex-membered set;

      cluster (A ** B) -> empty;

      coherence

      proof

        assume (A ** B) is non empty;

        then the Element of (A ** B) in (A ** B);

        then ex c1, c2 st the Element of (A ** B) = (c1 * c2) & c1 in A & c2 in B;

        hence thesis;

      end;

      cluster (B ** A) -> empty;

      coherence ;

    end

    registration

      let A,B be complex-membered non empty set;

      cluster (A ** B) -> non empty;

      coherence

      proof

        ( the Element of A * the Element of B) in (A ** B);

        hence thesis;

      end;

    end

    registration

      let A,B be complex-membered set;

      cluster (A ** B) -> complex-membered;

      coherence

      proof

        let e be object;

        assume e in (A ** B);

        then ex c1, c2 st e = (c1 * c2) & c1 in A & c2 in B;

        hence thesis;

      end;

    end

    registration

      let A,B be real-membered set;

      cluster (A ** B) -> real-membered;

      coherence

      proof

        let e be object;

        assume e in (A ** B);

        then ex c1, c2 st e = (c1 * c2) & c1 in A & c2 in B;

        hence thesis;

      end;

    end

    registration

      let A,B be rational-membered set;

      cluster (A ** B) -> rational-membered;

      coherence

      proof

        let e be object;

        assume e in (A ** B);

        then ex c1, c2 st e = (c1 * c2) & c1 in A & c2 in B;

        hence thesis;

      end;

    end

    registration

      let A,B be integer-membered set;

      cluster (A ** B) -> integer-membered;

      coherence

      proof

        let e be object;

        assume e in (A ** B);

        then ex c1, c2 st e = (c1 * c2) & c1 in A & c2 in B;

        hence thesis;

      end;

    end

    registration

      let A,B be natural-membered set;

      cluster (A ** B) -> natural-membered;

      coherence

      proof

        let e be object;

        assume e in (A ** B);

        then ex c1, c2 st e = (c1 * c2) & c1 in A & c2 in B;

        hence thesis;

      end;

    end

    registration

      let A,B be real-membered set, F,G be ext-real-membered set;

      identify F ** G with A ** B when A = F, B = G;

      compatibility

      proof

        assume

         A1: A = F & B = G;

        let a be ExtReal;

        hereby

          assume a in (A ** B);

          then

          consider c, c1 such that

           A2: a = (c * c1) and

           A3: c in A & c1 in B;

          reconsider d1 = c, d2 = c1 as Element of ExtREAL by A3, XXREAL_0:def 1;

          a = (d1 * d2) by A2, A3, XXREAL_3:def 5;

          hence a in (F ** G) by A1, A3;

        end;

        assume a in (F ** G);

        then

        consider w, w1 such that

         A4: a = (w * w1) and

         A5: w in F & w1 in G;

        reconsider d1 = w, d2 = w1 as Element of COMPLEX by A1, A5, XCMPLX_0:def 2;

        a = (d1 * d2) by A1, A4, A5, XXREAL_3:def 5;

        hence thesis by A1, A5;

      end;

    end

    theorem :: MEMBER_1:90



     Th90: ((A ** B) ** C) = (A ** (B ** C))

    proof

      let a;

      hereby

        assume a in ((A ** B) ** C);

        then

        consider c, c1 such that

         A1: a = (c * c1) and

         A2: c in (A ** B) and

         A3: c1 in C;

        consider c2,c3 be Complex such that

         A4: c = (c2 * c3) and

         A5: c2 in A and

         A6: c3 in B by A2;

        a = (c2 * (c3 * c1)) & (c3 * c1) in (B ** C) by A1, A3, A4, A6;

        hence a in (A ** (B ** C)) by A5;

      end;

      assume a in (A ** (B ** C));

      then

      consider c, c1 such that

       A7: a = (c * c1) & c in A and

       A8: c1 in (B ** C);

      consider c2,c3 be Complex such that

       A9: c1 = (c2 * c3) & c2 in B and

       A10: c3 in C by A8;

      a = ((c * c2) * c3) & (c * c2) in (A ** B) by A7, A9;

      hence thesis by A10;

    end;

    theorem :: MEMBER_1:91

    A c= B & C c= D implies (A ** C) c= (B ** D)

    proof

      assume

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

      let a;

      assume a in (A ** C);

      then ex c, c1 st a = (c * c1) & c in A & c1 in C;

      hence thesis by A1;

    end;

    theorem :: MEMBER_1:92



     Th92: (A ** (B \/ C)) = ((A ** B) \/ (A ** C))

    proof

      let a;

      hereby

        assume a in (A ** (B \/ C));

        then

        consider c, c1 such that

         A1: a = (c * c1) and

         A2: c in A and

         A3: c1 in (B \/ C);

        c1 in B or c1 in C by A3, XBOOLE_0:def 3;

        then (c * c1) in (A ** B) or (c * c1) in (A ** C) by A2;

        hence a in ((A ** B) \/ (A ** C)) by A1, XBOOLE_0:def 3;

      end;

      assume

       A4: a in ((A ** B) \/ (A ** C));

      per cases by A4, XBOOLE_0:def 3;

        suppose a in (A ** B);

        then

        consider c, c1 such that

         A5: a = (c * c1) & c in A and

         A6: c1 in B;

        c1 in (B \/ C) by A6, XBOOLE_0:def 3;

        hence thesis by A5;

      end;

        suppose a in (A ** C);

        then

        consider c, c1 such that

         A7: a = (c * c1) & c in A and

         A8: c1 in C;

        c1 in (B \/ C) by A8, XBOOLE_0:def 3;

        hence thesis by A7;

      end;

    end;

    theorem :: MEMBER_1:93



     Th93: (A ** (B /\ C)) c= ((A ** B) /\ (A ** C))

    proof

      let a;

      assume a in (A ** (B /\ C));

      then

      consider c, c1 such that

       A1: a = (c * c1) and

       A2: c in A and

       A3: c1 in (B /\ C);

      c1 in C by A3, XBOOLE_0:def 4;

      then

       A4: (c * c1) in (A ** C) by A2;

      c1 in B by A3, XBOOLE_0:def 4;

      then (c * c1) in (A ** B) by A2;

      hence thesis by A1, A4, XBOOLE_0:def 4;

    end;

    theorem :: MEMBER_1:94



     Th94: (A ** ( -- B)) = ( -- (A ** B))

    proof

      let a;

      hereby

        assume a in (A ** ( -- B));

        then

        consider c, c1 such that

         A1: a = (c * c1) and

         A2: c in A and

         A3: c1 in ( -- B);

        ( - c1) in B by A3, Th12;

        then

         A4: (c * ( - c1)) in (A ** B) by A2;

        a = ( - (c * ( - c1))) by A1;

        hence a in ( -- (A ** B)) by A4;

      end;

      assume a in ( -- (A ** B));

      then ( - a) in (A ** B) by Th12;

      then

      consider c, c1 such that

       A5: ( - a) = (c * c1) and

       A6: c in A and

       A7: c1 in B;

      a = (c * ( - c1)) & ( - c1) in ( -- B) by A5, A7;

      hence thesis by A6;

    end;

    theorem :: MEMBER_1:95



     Th95: (A ** (B ++ C)) c= ((A ** B) ++ (A ** C))

    proof

      let a;

      assume a in (A ** (B ++ C));

      then

      consider c, c1 such that

       A1: a = (c * c1) and

       A2: c in A and

       A3: c1 in (B ++ C);

      consider c2,c3 be Complex such that

       A4: c1 = (c2 + c3) & c2 in B and

       A5: c3 in C by A3;



       A6: (c * c3) in (A ** C) by A2, A5;

      a = ((c * c2) + (c * c3)) & (c * c2) in (A ** B) by A1, A2, A4;

      hence thesis by A6;

    end;

    theorem :: MEMBER_1:96



     Th96: (A ** (B -- C)) c= ((A ** B) -- (A ** C))

    proof

      (A ** (B ++ ( -- C))) c= ((A ** B) ++ (A ** ( -- C))) by Th95;

      hence thesis by Th94;

    end;

    theorem :: MEMBER_1:97



     Th97: ((A ** B) "" ) = ((A "" ) ** (B "" ))

    proof

      let a;

      hereby

        assume a in ((A ** B) "" );

        then

        consider c such that

         A1: a = (c " ) and

         A2: c in (A ** B);

        consider c1, c2 such that

         A3: c = (c1 * c2) and

         A4: c1 in A & c2 in B by A2;



         A5: (c1 " ) in (A "" ) & (c2 " ) in (B "" ) by A4;

        a = ((c1 " ) * (c2 " )) by A1, A3, XCMPLX_1: 204;

        hence a in ((A "" ) ** (B "" )) by A5;

      end;

      assume a in ((A "" ) ** (B "" ));

      then

      consider c, c1 such that

       A6: a = (c * c1) and

       A7: c in (A "" ) and

       A8: c1 in (B "" );

      consider c3 be Complex such that

       A9: c1 = (c3 " ) and

       A10: c3 in B by A8;

      consider c2 such that

       A11: c = (c2 " ) and

       A12: c2 in A by A7;



       A13: (c2 * c3) in (A ** B) by A12, A10;

      a = ((c2 * c3) " ) by A6, A11, A9, XCMPLX_1: 204;

      hence thesis by A13;

    end;

    theorem :: MEMBER_1:98



     Th98: ( {a} ** {b}) = {(a * b)}

    proof

      let z;

      hereby

        assume z in ( {a} ** {b});

        then

        consider c1, c2 such that

         A1: z = (c1 * c2) and

         A2: c1 in {a} & c2 in {b};

        c1 = a & c2 = b by A2, TARSKI:def 1;

        hence z in {(a * b)} by A1, TARSKI:def 1;

      end;



       A3: a in {a} & b in {b} by TARSKI:def 1;

      assume z in {(a * b)};

      then

       A4: z = (a * b) by TARSKI:def 1;

      thus thesis by A4, A3;

    end;

    theorem :: MEMBER_1:99



     Th99: ( {a} ** {s, t}) = {(a * s), (a * t)}

    proof



      thus ( {a} ** {s, t}) = ( {a} ** ( {s} \/ {t})) by ENUMSET1: 1

      .= (( {a} ** {s}) \/ ( {a} ** {t})) by Th92

      .= ( {(a * s)} \/ ( {a} ** {t})) by Th98

      .= ( {(a * s)} \/ {(a * t)}) by Th98

      .= {(a * s), (a * t)} by ENUMSET1: 1;

    end;

    theorem :: MEMBER_1:100



     Th100: ( {a, b} ** {s, t}) = {(a * s), (a * t), (b * s), (b * t)}

    proof



      thus ( {a, b} ** {s, t}) = (( {a} \/ {b}) ** {s, t}) by ENUMSET1: 1

      .= (( {a} ** {s, t}) \/ ( {b} ** {s, t})) by Th92

      .= ( {(a * s), (a * t)} \/ ( {b} ** {s, t})) by Th99

      .= ( {(a * s), (a * t)} \/ {(b * s), (b * t)}) by Th99

      .= {(a * s), (a * t), (b * s), (b * t)} by ENUMSET1: 5;

    end;

    definition

      let F,G be ext-real-membered set;

      :: MEMBER_1:def11

      func F /// G -> set equals (F ** (G "" ));

      coherence ;

    end

    theorem :: MEMBER_1:101



     Th101: (F /// G) = { (w1 / w2) : w1 in F & w2 in G }

    proof

      thus (F /// G) c= { (w1 / w2) : w1 in F & w2 in G }

      proof

        let e be object;

        assume e in (F /// G);

        then

        consider w1, w2 such that

         A1: e = (w1 * w2) and

         A2: w1 in F and

         A3: w2 in (G "" );

        consider w such that

         A4: w2 = (w " ) and

         A5: w in G by A3;

        e = (w1 / w) by A1, A4;

        hence thesis by A2, A5;

      end;

      let e be object;

      assume e in { (w1 / w2) : w1 in F & w2 in G };

      then

      consider w1, w2 such that

       A6: e = (w1 / w2) & w1 in F and

       A7: w2 in G;

      (w2 " ) in (G "" ) by A7;

      hence thesis by A6;

    end;

    theorem :: MEMBER_1:102



     Th102: f in F & g in G implies (f / g) in (F /// G)

    proof



       A1: f in ExtREAL & g in ExtREAL by XXREAL_0:def 1;

      (F /// G) = { (w1 / w2) : w1 in F & w2 in G } by Th101;

      hence thesis by A1;

    end;

    registration

      let F be empty set;

      let G be ext-real-membered set;

      cluster (F /// G) -> empty;

      coherence ;

      cluster (G /// F) -> empty;

      coherence ;

    end

    registration

      let F,G be ext-real-membered non empty set;

      cluster (F /// G) -> non empty;

      coherence ;

    end

    registration

      let F,G be ext-real-membered set;

      cluster (F /// G) -> ext-real-membered;

      coherence ;

    end

    theorem :: MEMBER_1:103

    F c= G & H c= I implies (F /// H) c= (G /// I)

    proof

      assume

       A1: F c= G & H c= I;

      let i;



       A2: (F /// H) = { (w1 / w2) : w1 in F & w2 in H } by Th101;

      assume i in (F /// H);

      then ex w, w1 st i = (w / w1) & w in F & w1 in H by A2;

      hence thesis by A1, Th102;

    end;

    theorem :: MEMBER_1:104

    ((F \/ G) /// H) = ((F /// H) \/ (G /// H)) by Th82;

    theorem :: MEMBER_1:105

    ((F /\ G) /// H) c= ((F /// H) /\ (G /// H)) by Th83;

    theorem :: MEMBER_1:106

    (F /// (G \/ H)) = ((F /// G) \/ (F /// H))

    proof



      thus (F /// (G \/ H)) = (F ** ((G "" ) \/ (H "" ))) by Th23

      .= ((F /// G) \/ (F /// H)) by Th82;

    end;

    theorem :: MEMBER_1:107

    (F /// (G /\ H)) c= ((F /// G) /\ (F /// H))

    proof

      ((G /\ H) "" ) c= ((G "" ) /\ (H "" )) by Th24;

      then

       A1: (F ** ((G /\ H) "" )) c= (F ** ((G "" ) /\ (H "" ))) by Th81;

      (F ** ((G "" ) /\ (H "" ))) c= ((F ** (G "" )) /\ (F ** (H "" ))) by Th83;

      hence thesis by A1;

    end;

    theorem :: MEMBER_1:108

    ((F ** G) /// H) = (F ** (G /// H)) by Th80;

    theorem :: MEMBER_1:109

    ((F /// G) ** H) = ((F ** H) /// G) by Th80;

    theorem :: MEMBER_1:110

    ((F /// G) /// H) = (F /// (G ** H))

    proof



      thus ((F /// G) /// H) = (F ** ((G "" ) ** (H "" ))) by Th80

      .= (F /// (G ** H)) by Th85;

    end;

    theorem :: MEMBER_1:111

    ( {f} /// {g}) = {(f / g)}

    proof



      thus ( {f} /// {g}) = ( {f} ** {(g " )}) by Th26

      .= {(f / g)} by Th86;

    end;

    theorem :: MEMBER_1:112

    ( {f} /// {h, i}) = {(f / h), (f / i)}

    proof



      thus ( {f} /// {h, i}) = ( {f} ** {(h " ), (i " )}) by Th27

      .= {(f / h), (f / i)} by Th87;

    end;

    theorem :: MEMBER_1:113

    ( {f, g} /// {h}) = {(f / h), (g / h)}

    proof



      thus ( {f, g} /// {h}) = ( {f, g} ** {(h " )}) by Th26

      .= {(f / h), (g / h)} by Th87;

    end;

    theorem :: MEMBER_1:114

    ( {f, g} /// {h, i}) = {(f / h), (f / i), (g / h), (g / i)}

    proof



      thus ( {f, g} /// {h, i}) = ( {f, g} ** {(h " ), (i " )}) by Th27

      .= {(f / h), (f / i), (g / h), (g / i)} by Th88;

    end;

    definition

      let A,B be complex-membered set;

      :: MEMBER_1:def12

      func A /// B -> set equals (A ** (B "" ));

      coherence ;

    end

    theorem :: MEMBER_1:115



     Th115: (A /// B) = { (c1 / c2) : c1 in A & c2 in B }

    proof

      thus (A /// B) c= { (c1 / c2) : c1 in A & c2 in B }

      proof

        let e be object;

        assume e in (A /// B);

        then

        consider c1, c2 such that

         A1: e = (c1 * c2) and

         A2: c1 in A and

         A3: c2 in (B "" );

        e = (c1 / (c2 " )) & (c2 " ) in B by A1, A3, Th29;

        hence thesis by A2;

      end;

      let e be object;

      assume e in { (c1 / c2) : c1 in A & c2 in B };

      then

      consider c1, c2 such that

       A4: e = (c1 / c2) & c1 in A and

       A5: c2 in B;

      (c2 " ) in (B "" ) by A5;

      hence thesis by A4;

    end;

    theorem :: MEMBER_1:116



     Th116: a in A & b in B implies (a / b) in (A /// B)

    proof

      (A /// B) = { (c1 / c2) : c1 in A & c2 in B } by Th115;

      hence thesis;

    end;

    registration

      let A be empty set;

      let B be complex-membered set;

      cluster (A /// B) -> empty;

      coherence ;

      cluster (B /// A) -> empty;

      coherence ;

    end

    registration

      let A,B be complex-membered non empty set;

      cluster (A /// B) -> non empty;

      coherence ;

    end

    registration

      let A,B be complex-membered set;

      cluster (A /// B) -> complex-membered;

      coherence ;

    end

    registration

      let A,B be real-membered set;

      cluster (A /// B) -> real-membered;

      coherence ;

    end

    registration

      let A,B be rational-membered set;

      cluster (A /// B) -> rational-membered;

      coherence ;

    end

    registration

      let A,B be real-membered set, F,G be ext-real-membered set;

      identify F /// G with A /// B when A = F, B = G;

      compatibility ;

    end

    theorem :: MEMBER_1:117

    A c= B & C c= D implies (A /// C) c= (B /// D)

    proof

      assume

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

      let z;



       A2: (A /// C) = { (c1 / c2) : c1 in A & c2 in C } by Th115;

      assume z in (A /// C);

      then ex c, c1 st z = (c / c1) & c in A & c1 in C by A2;

      hence thesis by A1, Th116;

    end;

    theorem :: MEMBER_1:118

    (A /// (B \/ C)) = ((A /// B) \/ (A /// C))

    proof



      thus (A /// (B \/ C)) = (A ** ((B "" ) \/ (C "" ))) by Th32

      .= ((A /// B) \/ (A /// C)) by Th92;

    end;

    theorem :: MEMBER_1:119

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

    proof

      (A /// (B /\ C)) = (A ** ((B "" ) /\ (C "" ))) by Th33;

      hence thesis by Th93;

    end;

    theorem :: MEMBER_1:120

    (A /// ( -- B)) = ( -- (A /// B))

    proof



      thus (A /// ( -- B)) = (A ** ( -- (B "" ))) by Th36

      .= ( -- (A /// B)) by Th94;

    end;

    theorem :: MEMBER_1:121

    (( -- A) /// B) = ( -- (A /// B)) by Th94;

    theorem :: MEMBER_1:122

    ((A ++ B) /// C) c= ((A /// C) ++ (B /// C)) by Th95;

    theorem :: MEMBER_1:123

    ((A -- B) /// C) c= ((A /// C) -- (B /// C))

    proof

      ((A ++ ( -- B)) /// C) c= ((A /// C) ++ (( -- B) /// C)) by Th95;

      hence thesis by Th94;

    end;

    theorem :: MEMBER_1:124

    ((A ** B) /// C) = (A ** (B /// C)) by Th90;

    theorem :: MEMBER_1:125

    ((A /// B) ** C) = ((A ** C) /// B) by Th90;

    theorem :: MEMBER_1:126

    ((A /// B) /// C) = (A /// (B ** C))

    proof



      thus ((A /// B) /// C) = (A ** ((B "" ) ** (C "" ))) by Th90

      .= (A /// (B ** C)) by Th97;

    end;

    theorem :: MEMBER_1:127

    (A /// (B /// C)) = ((A ** C) /// B)

    proof



      thus (A /// (B /// C)) = (A ** ((B "" ) ** ((C "" ) "" ))) by Th97

      .= ((A ** C) /// B) by Th90;

    end;

    theorem :: MEMBER_1:128

    ( {a} /// {b}) = {(a / b)}

    proof



      thus ( {a} /// {b}) = ( {a} ** {(b " )}) by Th37

      .= {(a / b)} by Th98;

    end;

    theorem :: MEMBER_1:129

    ( {a} /// {s, t}) = {(a / s), (a / t)}

    proof



      thus ( {a} /// {s, t}) = ( {a} ** {(s " ), (t " )}) by Th38

      .= {(a / s), (a / t)} by Th99;

    end;

    theorem :: MEMBER_1:130

    ( {a, b} /// {s}) = {(a / s), (b / s)}

    proof



      thus ( {a, b} /// {s}) = ( {a, b} ** {(s " )}) by Th37

      .= {(a / s), (b / s)} by Th99;

    end;

    theorem :: MEMBER_1:131

    ( {a, b} /// {s, t}) = {(a / s), (a / t), (b / s), (b / t)}

    proof



      thus ( {a, b} /// {s, t}) = ( {a, b} ** {(s " ), (t " )}) by Th38

      .= {(a / s), (a / t), (b / s), (b / t)} by Th100;

    end;

    definition

      let F be ext-real-membered set;

      let f be ExtReal;

      :: MEMBER_1:def13

      func f ++ F -> set equals ( {f} ++ F);

      coherence ;

    end

    theorem :: MEMBER_1:132



     Th132: g in G implies (f + g) in (f ++ G)

    proof

      f in {f} by TARSKI:def 1;

      hence thesis by Th39;

    end;

    theorem :: MEMBER_1:133



     Th133: (f ++ F) = { (f + w) : w in F }

    proof

      thus (f ++ F) c= { (f + w) : w in F }

      proof

        let e be object;

        assume e in (f ++ F);

        then

        consider w1, w2 such that

         A1: e = (w1 + w2) and

         A2: w1 in {f} and

         A3: w2 in F;

        w1 = f by A2, TARSKI:def 1;

        hence thesis by A1, A3;

      end;

      let e be object;

      assume e in { (f + w) : w in F };

      then ex w st e = (f + w) & w in F;

      hence thesis by Th132;

    end;

    theorem :: MEMBER_1:134



     Th134: e in (f ++ F) implies ex w st e = (f + w) & w in F

    proof

      (f ++ F) = { (f + w) : w in F } by Th133;

      hence thesis;

    end;

    registration

      let F be empty set;

      let f be ExtReal;

      cluster (f ++ F) -> empty;

      coherence ;

    end

    registration

      let F be ext-real-membered non empty set;

      let f be ExtReal;

      cluster (f ++ F) -> non empty;

      coherence ;

    end

    registration

      let F be ext-real-membered set;

      let f be ExtReal;

      cluster (f ++ F) -> ext-real-membered;

      coherence ;

    end

    theorem :: MEMBER_1:135



     Th135: (r ++ F) c= (r ++ G) implies F c= G

    proof

      assume

       A1: (r ++ F) c= (r ++ G);

      let i;

      assume i in F;

      then (r + i) in (r ++ F) by Th132;

      then ex w st (r + i) = (r + w) & w in G by A1, Th134;

      hence thesis by XXREAL_3: 11;

    end;

    theorem :: MEMBER_1:136

    (r ++ F) = (r ++ G) implies F = G

    proof

      assume (r ++ F) = (r ++ G);

      then F c= G & G c= F by Th135;

      hence thesis;

    end;

    theorem :: MEMBER_1:137



     Th137: (r ++ (F /\ G)) = ((r ++ F) /\ (r ++ G))

    proof



       A1: ((r ++ F) /\ (r ++ G)) c= (r ++ (F /\ G))

      proof

        let j;

        assume

         A2: j in ((r ++ F) /\ (r ++ G));

        then j in (r ++ F) by XBOOLE_0:def 4;

        then

        consider w such that

         A3: j = (r + w) and

         A4: w in F by Th134;

        j in (r ++ G) by A2, XBOOLE_0:def 4;

        then

        consider w1 such that

         A5: j = (r + w1) and

         A6: w1 in G by Th134;

        w = w1 by A3, A5, XXREAL_3: 11;

        then w in (F /\ G) by A4, A6, XBOOLE_0:def 4;

        hence thesis by A3, Th132;

      end;

      (r ++ (F /\ G)) c= ((r ++ F) /\ (r ++ G)) by Th42;

      hence thesis by A1;

    end;

    theorem :: MEMBER_1:138



     Th138: ((f ++ F) \ (f ++ G)) c= (f ++ (F \ G))

    proof

      let i;

      assume

       A1: i in ((f ++ F) \ (f ++ G));

      then

      consider w such that

       A2: i = (f + w) and

       A3: w in F by Th134;

      now

        assume not w in (F \ G);

        then w in G by A3, XBOOLE_0:def 5;

        then (f + w) in (f ++ G) by Th132;

        hence contradiction by A1, A2, XBOOLE_0:def 5;

      end;

      hence thesis by A2, Th132;

    end;

    theorem :: MEMBER_1:139



     Th139: (r ++ (F \ G)) = ((r ++ F) \ (r ++ G))

    proof



       A1: (r ++ (F \ G)) c= ((r ++ F) \ (r ++ G))

      proof

        let i;

        assume i in (r ++ (F \ G));

        then

        consider w such that

         A2: i = (r + w) and

         A3: w in (F \ G) by Th134;

         A4:

        now

          assume (r + w) in (r ++ G);

          then

          consider w1 such that

           A5: (r + w) = (r + w1) and

           A6: w1 in G by Th134;

          w = w1 by A5, XXREAL_3: 11;

          hence contradiction by A3, A6, XBOOLE_0:def 5;

        end;

        (r + w) in (r ++ F) by A3, Th132;

        hence thesis by A2, A4, XBOOLE_0:def 5;

      end;

      ((r ++ F) \ (r ++ G)) c= (r ++ (F \ G)) by Th138;

      hence thesis by A1;

    end;

    theorem :: MEMBER_1:140



     Th140: (r ++ (F \+\ G)) = ((r ++ F) \+\ (r ++ G))

    proof



      thus (r ++ (F \+\ G)) = ((r ++ (F \ G)) \/ (r ++ (G \ F))) by Th41

      .= (((r ++ F) \ (r ++ G)) \/ (r ++ (G \ F))) by Th139

      .= ((r ++ F) \+\ (r ++ G)) by Th139;

    end;

    definition

      let A be complex-membered set;

      let a be Complex;

      :: MEMBER_1:def14

      func a ++ A -> set equals ( {a} ++ A);

      coherence ;

    end

    theorem :: MEMBER_1:141



     Th141: b in A implies (a + b) in (a ++ A)

    proof

      a in {a} by TARSKI:def 1;

      hence thesis;

    end;

    theorem :: MEMBER_1:142



     Th142: (a ++ A) = { (a + c) : c in A }

    proof

      thus (a ++ A) c= { (a + c) : c in A }

      proof

        let e be object;

        assume e in (a ++ A);

        then

        consider c1, c2 such that

         A1: e = (c1 + c2) and

         A2: c1 in {a} and

         A3: c2 in A;

        c1 = a by A2, TARSKI:def 1;

        hence thesis by A1, A3;

      end;

      let e be object;

      assume e in { (a + c) : c in A };

      then ex c st e = (a + c) & c in A;

      hence thesis by Th141;

    end;

    theorem :: MEMBER_1:143



     Th143: e in (a ++ A) implies ex c st e = (a + c) & c in A

    proof

      (a ++ A) = { (a + c) : c in A } by Th142;

      hence thesis;

    end;

    registration

      let A be empty set;

      let a be Complex;

      cluster (a ++ A) -> empty;

      coherence ;

    end

    registration

      let A be complex-membered non empty set;

      let a be Complex;

      cluster (a ++ A) -> non empty;

      coherence ;

    end

    registration

      let A be complex-membered set;

      let a be Complex;

      cluster (a ++ A) -> complex-membered;

      coherence ;

    end

    registration

      let A be real-membered set;

      let a be Real;

      cluster (a ++ A) -> real-membered;

      coherence ;

    end

    registration

      let A be rational-membered set;

      let a be Rational;

      cluster (a ++ A) -> rational-membered;

      coherence ;

    end

    registration

      let A be integer-membered set;

      let a be Integer;

      cluster (a ++ A) -> integer-membered;

      coherence ;

    end

    registration

      let A be natural-membered set;

      let a be Nat;

      cluster (a ++ A) -> natural-membered;

      coherence ;

    end

    registration

      let A be real-membered set, F be ext-real-membered set;

      let a be Real, f be ExtReal;

      identify f ++ F with a ++ A when a = f, A = F;

      compatibility ;

    end

    theorem :: MEMBER_1:144



     Th144: A c= B iff (a ++ A) c= (a ++ B)

    proof

      thus A c= B implies (a ++ A) c= (a ++ B) by Th47;

      assume

       A1: (a ++ A) c= (a ++ B);

      let z;

      assume z in A;

      then (a + z) in (a ++ A) by Th141;

      then ex c st (a + z) = (a + c) & c in B by A1, Th143;

      hence thesis;

    end;

    theorem :: MEMBER_1:145

    (a ++ A) = (a ++ B) implies A = B

    proof

      assume (a ++ A) = (a ++ B);

      then A c= B & B c= A by Th144;

      hence thesis;

    end;

    theorem :: MEMBER_1:146

    ( 0 ++ A) = A

    proof

      let a;

      hereby

        assume a in ( 0 ++ A);

        then

        consider c1, c2 such that

         A1: a = (c1 + c2) and

         A2: c1 in { 0 } and

         A3: c2 in A;

        c1 = 0 by A2, TARSKI:def 1;

        hence a in A by A1, A3;

      end;

      assume a in A;

      then ( 0 + a) in { ( 0 + c) : c in A };

      hence thesis by Th142;

    end;

    theorem :: MEMBER_1:147

    ((a + b) ++ A) = (a ++ (b ++ A))

    proof



      thus ((a + b) ++ A) = (( {a} ++ {b}) ++ A) by Th51

      .= (a ++ (b ++ A)) by Th50;

    end;

    theorem :: MEMBER_1:148

    (a ++ (A ++ B)) = ((a ++ A) ++ B) by Th50;

    theorem :: MEMBER_1:149



     Th149: (a ++ (A /\ B)) = ((a ++ A) /\ (a ++ B))

    proof



       A1: ((a ++ A) /\ (a ++ B)) c= (a ++ (A /\ B))

      proof

        let z;

        assume

         A2: z in ((a ++ A) /\ (a ++ B));

        then z in (a ++ A) by XBOOLE_0:def 4;

        then

        consider c such that

         A3: z = (a + c) and

         A4: c in A by Th143;

        z in (a ++ B) by A2, XBOOLE_0:def 4;

        then ex c1 st z = (a + c1) & c1 in B by Th143;

        then c in (A /\ B) by A3, A4, XBOOLE_0:def 4;

        hence thesis by A3, Th141;

      end;

      (a ++ (A /\ B)) c= ((a ++ A) /\ (a ++ B)) by Th49;

      hence thesis by A1;

    end;

    theorem :: MEMBER_1:150



     Th150: (a ++ (A \ B)) = ((a ++ A) \ (a ++ B))

    proof

      let z;

      hereby

        assume z in (a ++ (A \ B));

        then

        consider c such that

         A1: z = (a + c) and

         A2: c in (A \ B) by Th143;

         A3:

        now

          assume (a + c) in (a ++ B);

          then ex c1 st (a + c) = (a + c1) & c1 in B by Th143;

          hence contradiction by A2, XBOOLE_0:def 5;

        end;

        (a + c) in (a ++ A) by A2, Th141;

        hence z in ((a ++ A) \ (a ++ B)) by A1, A3, XBOOLE_0:def 5;

      end;

      assume

       A4: z in ((a ++ A) \ (a ++ B));

      then

      consider c such that

       A5: z = (a + c) and

       A6: c in A by Th143;

      now

        assume not c in (A \ B);

        then c in B by A6, XBOOLE_0:def 5;

        then (a + c) in (a ++ B) by Th141;

        hence contradiction by A4, A5, XBOOLE_0:def 5;

      end;

      hence thesis by A5, Th141;

    end;

    theorem :: MEMBER_1:151



     Th151: (a ++ (A \+\ B)) = ((a ++ A) \+\ (a ++ B))

    proof



      thus (a ++ (A \+\ B)) = ((a ++ (A \ B)) \/ (a ++ (B \ A))) by Th48

      .= (((a ++ A) \ (a ++ B)) \/ (a ++ (B \ A))) by Th150

      .= ((a ++ A) \+\ (a ++ B)) by Th150;

    end;

    definition

      let F be ext-real-membered set;

      let f be ExtReal;

      :: MEMBER_1:def15

      func f -- F -> set equals ( {f} -- F);

      coherence ;

    end

    theorem :: MEMBER_1:152



     Th152: g in G implies (f - g) in (f -- G)

    proof

      f in {f} by TARSKI:def 1;

      hence thesis by Th55;

    end;

    theorem :: MEMBER_1:153



     Th153: (f -- F) = { (f - w) : w in F }

    proof

      thus (f -- F) c= { (f - w) : w in F }

      proof

        let e be object;

        assume e in (f -- F);

        then

        consider w1, w2 such that

         A1: e = (w1 + w2) and

         A2: w1 in {f} & w2 in ( -- F);



         A3: (w1 - ( - w2)) = (w1 + w2);

        ( - w2) in F & w1 = f by A2, Th2, TARSKI:def 1;

        hence thesis by A1, A3;

      end;

      let e be object;

      assume e in { (f - w) : w in F };

      then ex w st e = (f - w) & w in F;

      hence thesis by Th152;

    end;

    theorem :: MEMBER_1:154



     Th154: e in (f -- F) implies ex w st e = (f - w) & w in F

    proof

      (f -- F) = { (f - w) : w in F } by Th153;

      hence thesis;

    end;

    registration

      let F be empty set;

      let f be ExtReal;

      cluster (f -- F) -> empty;

      coherence ;

    end

    registration

      let F be ext-real-membered non empty set;

      let f be ExtReal;

      cluster (f -- F) -> non empty;

      coherence ;

    end

    registration

      let F be ext-real-membered set;

      let f be ExtReal;

      cluster (f -- F) -> ext-real-membered;

      coherence ;

    end

    theorem :: MEMBER_1:155



     Th155: (r -- F) c= (r -- G) implies F c= G

    proof

      assume

       A1: (r -- F) c= (r -- G);

      let i;

      assume i in F;

      then (r - i) in (r -- F) by Th152;

      then ex w st (r - i) = (r - w) & w in G by A1, Th154;

      hence thesis by XXREAL_3: 12;

    end;

    theorem :: MEMBER_1:156

    (r -- F) = (r -- G) implies F = G

    proof

      assume (r -- F) = (r -- G);

      then F c= G & G c= F by Th155;

      hence thesis;

    end;

    theorem :: MEMBER_1:157



     Th157: (r -- (F /\ G)) = ((r -- F) /\ (r -- G))

    proof



      thus (r -- (F /\ G)) = (r ++ (( -- F) /\ ( -- G))) by Th6

      .= ((r ++ ( -- F)) /\ (r ++ ( -- G))) by Th137

      .= ((r -- F) /\ (r -- G));

    end;

    theorem :: MEMBER_1:158



     Th158: (r -- (F \ G)) = ((r -- F) \ (r -- G))

    proof



      thus (r -- (F \ G)) = (r ++ (( -- F) \ ( -- G))) by Th7

      .= ((r ++ ( -- F)) \ (r ++ ( -- G))) by Th139

      .= ((r -- F) \ (r -- G));

    end;

    theorem :: MEMBER_1:159



     Th159: (r -- (F \+\ G)) = ((r -- F) \+\ (r -- G))

    proof



      thus (r -- (F \+\ G)) = (r ++ (( -- F) \+\ ( -- G))) by Th8

      .= ((r ++ ( -- F)) \+\ (r ++ ( -- G))) by Th140

      .= ((r -- F) \+\ (r -- G));

    end;

    definition

      let A be complex-membered set;

      let a be Complex;

      :: MEMBER_1:def16

      func a -- A -> set equals ( {a} -- A);

      coherence ;

    end

    theorem :: MEMBER_1:160



     Th160: b in A implies (a - b) in (a -- A)

    proof

      a in {a} by TARSKI:def 1;

      hence thesis by Th66;

    end;

    theorem :: MEMBER_1:161



     Th161: (a -- A) = { (a - c) : c in A }

    proof



       A1: (a -- A) = { (c1 - c2) : c1 in {a} & c2 in A } by Th65;

      thus (a -- A) c= { (a - c) : c in A }

      proof

        let e be object;

        assume e in (a -- A);

        then

        consider c1, c2 such that

         A2: e = (c1 - c2) and

         A3: c1 in {a} and

         A4: c2 in A by A1;

        c1 = a by A3, TARSKI:def 1;

        hence thesis by A2, A4;

      end;

      let e be object;

      assume e in { (a - c) : c in A };

      then ex c st e = (a - c) & c in A;

      hence thesis by Th160;

    end;

    theorem :: MEMBER_1:162



     Th162: e in (a -- A) implies ex c st e = (a - c) & c in A

    proof

      (a -- A) = { (a - c) : c in A } by Th161;

      hence thesis;

    end;

    registration

      let A be empty set;

      let a be Complex;

      cluster (a -- A) -> empty;

      coherence ;

    end

    registration

      let A be complex-membered non empty set;

      let a be Complex;

      cluster (a -- A) -> non empty;

      coherence ;

    end

    registration

      let A be complex-membered set;

      let a be Complex;

      cluster (a -- A) -> complex-membered;

      coherence ;

    end

    registration

      let A be real-membered set;

      let a be Real;

      cluster (a -- A) -> real-membered;

      coherence ;

    end

    registration

      let A be rational-membered set;

      let a be Rational;

      cluster (a -- A) -> rational-membered;

      coherence ;

    end

    registration

      let A be integer-membered set;

      let a be Integer;

      cluster (a -- A) -> integer-membered;

      coherence ;

    end

    registration

      let A be real-membered set, F be ext-real-membered set;

      let a be Real, f be ExtReal;

      identify f -- F with a -- A when a = f, A = F;

      compatibility ;

    end

    theorem :: MEMBER_1:163



     Th163: A c= B iff (a -- A) c= (a -- B)

    proof

      thus A c= B implies (a -- A) c= (a -- B) by Th67;

      assume

       A1: (a -- A) c= (a -- B);

      let z;

      assume z in A;

      then (a - z) in (a -- A) by Th160;

      then ex c st (a - z) = (a - c) & c in B by A1, Th162;

      hence thesis;

    end;

    theorem :: MEMBER_1:164

    (a -- A) = (a -- B) implies A = B

    proof

      assume (a -- A) = (a -- B);

      then A c= B & B c= A by Th163;

      hence thesis;

    end;

    theorem :: MEMBER_1:165



     Th165: (a -- (A /\ B)) = ((a -- A) /\ (a -- B))

    proof



      thus (a -- (A /\ B)) = (a ++ (( -- A) /\ ( -- B))) by Th16

      .= ((a ++ ( -- A)) /\ (a ++ ( -- B))) by Th149

      .= ((a -- A) /\ (a -- B));

    end;

    theorem :: MEMBER_1:166



     Th166: (a -- (A \ B)) = ((a -- A) \ (a -- B))

    proof



      thus (a -- (A \ B)) = (a ++ (( -- A) \ ( -- B))) by Th17

      .= ((a ++ ( -- A)) \ (a ++ ( -- B))) by Th150

      .= ((a -- A) \ (a -- B));

    end;

    theorem :: MEMBER_1:167



     Th167: (a -- (A \+\ B)) = ((a -- A) \+\ (a -- B))

    proof



      thus (a -- (A \+\ B)) = (a ++ (( -- A) \+\ ( -- B))) by Th18

      .= ((a ++ ( -- A)) \+\ (a ++ ( -- B))) by Th151

      .= ((a -- A) \+\ (a -- B));

    end;

    definition

      let F be ext-real-membered set;

      let f be ExtReal;

      :: MEMBER_1:def17

      func F -- f -> set equals (F -- {f});

      coherence ;

    end

    theorem :: MEMBER_1:168



     Th168: g in G implies (g - f) in (G -- f)

    proof

      f in {f} by TARSKI:def 1;

      hence thesis by Th55;

    end;

    theorem :: MEMBER_1:169



     Th169: (F -- f) = { (w - f) : w in F }

    proof

      thus (F -- f) c= { (w - f) : w in F }

      proof

        let e be object;

        assume e in (F -- f);

        then

        consider w1, w2 such that

         A1: e = (w1 + w2) & w1 in F and

         A2: w2 in ( -- {f});

        ( - w2) in {f} by A2, Th2;

        then (w1 - ( - w2)) = (w1 + w2) & ( - w2) = f by TARSKI:def 1;

        hence thesis by A1;

      end;

      let e be object;

      assume e in { (w - f) : w in F };

      then ex w st e = (w - f) & w in F;

      hence thesis by Th168;

    end;

    theorem :: MEMBER_1:170

    e in (F -- f) implies ex w st e = (w - f) & w in F

    proof

      (F -- f) = { (w - f) : w in F } by Th169;

      hence thesis;

    end;

    registration

      let F be empty set;

      let f be ExtReal;

      cluster (F -- f) -> empty;

      coherence ;

    end

    registration

      let F be ext-real-membered non empty set;

      let f be ExtReal;

      cluster (F -- f) -> non empty;

      coherence ;

    end

    registration

      let F be ext-real-membered set;

      let f be ExtReal;

      cluster (F -- f) -> ext-real-membered;

      coherence ;

    end

    theorem :: MEMBER_1:171

    (F -- f) = ( -- (f -- F)) by Th60;

    theorem :: MEMBER_1:172

    (f -- F) = ( -- (F -- f)) by Th60;

    theorem :: MEMBER_1:173

    ((F /\ G) -- r) = ((F -- r) /\ (G -- r))

    proof



      thus ((F /\ G) -- r) = ( -- (r -- (F /\ G))) by Th60

      .= ( -- ((r -- F) /\ (r -- G))) by Th157

      .= (( -- (r -- F)) /\ ( -- (r -- G))) by Th6

      .= (( -- (r -- F)) /\ (G -- r)) by Th60

      .= ((F -- r) /\ (G -- r)) by Th60;

    end;

    theorem :: MEMBER_1:174

    ((F \ G) -- r) = ((F -- r) \ (G -- r))

    proof



      thus ((F \ G) -- r) = ( -- (r -- (F \ G))) by Th60

      .= ( -- ((r -- F) \ (r -- G))) by Th158

      .= (( -- (r -- F)) \ ( -- (r -- G))) by Th7

      .= (( -- (r -- F)) \ (G -- r)) by Th60

      .= ((F -- r) \ (G -- r)) by Th60;

    end;

    theorem :: MEMBER_1:175

    ((F \+\ G) -- r) = ((F -- r) \+\ (G -- r))

    proof



      thus ((F \+\ G) -- r) = ( -- (r -- (F \+\ G))) by Th60

      .= ( -- ((r -- F) \+\ (r -- G))) by Th159

      .= (( -- (r -- F)) \+\ ( -- (r -- G))) by Th8

      .= (( -- (r -- F)) \+\ (G -- r)) by Th60

      .= ((F -- r) \+\ (G -- r)) by Th60;

    end;

    definition

      let A be complex-membered set;

      let a be Complex;

      :: MEMBER_1:def18

      func A -- a -> set equals (A -- {a});

      coherence ;

    end

    theorem :: MEMBER_1:176



     Th176: b in A implies (b - a) in (A -- a)

    proof

      a in {a} by TARSKI:def 1;

      hence thesis by Th66;

    end;

    theorem :: MEMBER_1:177



     Th177: (A -- a) = { (c - a) : c in A }

    proof



       A1: (A -- a) = { (c1 - c2) : c1 in A & c2 in {a} } by Th65;

      thus (A -- a) c= { (c - a) : c in A }

      proof

        let e be object;

        assume e in (A -- a);

        then

        consider c1, c2 such that

         A2: e = (c1 - c2) & c1 in A and

         A3: c2 in {a} by A1;

        c2 = a by A3, TARSKI:def 1;

        hence thesis by A2;

      end;

      let e be object;

      assume e in { (c - a) : c in A };

      then ex c st e = (c - a) & c in A;

      hence thesis by Th176;

    end;

    theorem :: MEMBER_1:178



     Th178: e in (A -- a) implies ex c st e = (c - a) & c in A

    proof

      (A -- a) = { (c - a) : c in A } by Th177;

      hence thesis;

    end;

    registration

      let A be empty set;

      let a be Complex;

      cluster (A -- a) -> empty;

      coherence ;

    end

    registration

      let A be complex-membered non empty set;

      let a be Complex;

      cluster (A -- a) -> non empty;

      coherence ;

    end

    registration

      let A be complex-membered set;

      let a be Complex;

      cluster (A -- a) -> complex-membered;

      coherence ;

    end

    registration

      let A be real-membered set;

      let a be Real;

      cluster (A -- a) -> real-membered;

      coherence ;

    end

    registration

      let A be rational-membered set;

      let a be Rational;

      cluster (A -- a) -> rational-membered;

      coherence ;

    end

    registration

      let A be integer-membered set;

      let a be Integer;

      cluster (A -- a) -> integer-membered;

      coherence ;

    end

    registration

      let A be real-membered set, F be ext-real-membered set;

      let a be Real, f be ExtReal;

      identify F -- f with A -- a when a = f, A = F;

      compatibility ;

    end

    theorem :: MEMBER_1:179



     Th179: A c= B iff (A -- a) c= (B -- a)

    proof

      thus A c= B implies (A -- a) c= (B -- a) by Th67;

      assume

       A1: (A -- a) c= (B -- a);

      let z;

      assume z in A;

      then (z - a) in (A -- a) by Th176;

      then ex c st (z - a) = (c - a) & c in B by A1, Th178;

      hence thesis;

    end;

    theorem :: MEMBER_1:180

    (A -- a) = (B -- a) implies A = B

    proof

      assume (A -- a) = (B -- a);

      then A c= B & B c= A by Th179;

      hence thesis;

    end;

    theorem :: MEMBER_1:181

    (A -- a) = ( -- (a -- A)) by Th71;

    theorem :: MEMBER_1:182

    (a -- A) = ( -- (A -- a)) by Th71;

    theorem :: MEMBER_1:183

    ((A /\ B) -- a) = ((A -- a) /\ (B -- a))

    proof



      thus ((A /\ B) -- a) = ( -- (a -- (A /\ B))) by Th71

      .= ( -- ((a -- A) /\ (a -- B))) by Th165

      .= (( -- (a -- A)) /\ ( -- (a -- B))) by Th16

      .= (( -- (a -- A)) /\ (B -- a)) by Th71

      .= ((A -- a) /\ (B -- a)) by Th71;

    end;

    theorem :: MEMBER_1:184

    ((A \ B) -- a) = ((A -- a) \ (B -- a))

    proof



      thus ((A \ B) -- a) = ( -- (a -- (A \ B))) by Th71

      .= ( -- ((a -- A) \ (a -- B))) by Th166

      .= (( -- (a -- A)) \ ( -- (a -- B))) by Th17

      .= (( -- (a -- A)) \ (B -- a)) by Th71

      .= ((A -- a) \ (B -- a)) by Th71;

    end;

    theorem :: MEMBER_1:185

    ((A \+\ B) -- a) = ((A -- a) \+\ (B -- a))

    proof



      thus ((A \+\ B) -- a) = ( -- (a -- (A \+\ B))) by Th71

      .= ( -- ((a -- A) \+\ (a -- B))) by Th167

      .= (( -- (a -- A)) \+\ ( -- (a -- B))) by Th18

      .= (( -- (a -- A)) \+\ (B -- a)) by Th71

      .= ((A -- a) \+\ (B -- a)) by Th71;

    end;

    definition

      let F be ext-real-membered set;

      let f be ExtReal;

      :: MEMBER_1:def19

      func f ** F -> set equals ( {f} ** F);

      coherence ;

    end

    theorem :: MEMBER_1:186



     Th186: g in G implies (f * g) in (f ** G)

    proof

      f in {f} by TARSKI:def 1;

      hence thesis by Th79;

    end;

    theorem :: MEMBER_1:187



     Th187: (f ** F) = { (f * w) : w in F }

    proof

      thus (f ** F) c= { (f * w) : w in F }

      proof

        let e be object;

        assume e in (f ** F);

        then

        consider w1, w2 such that

         A1: e = (w1 * w2) and

         A2: w1 in {f} and

         A3: w2 in F;

        w1 = f by A2, TARSKI:def 1;

        hence thesis by A1, A3;

      end;

      let e be object;

      assume e in { (f * w) : w in F };

      then ex w st e = (f * w) & w in F;

      hence thesis by Th186;

    end;

    theorem :: MEMBER_1:188



     Th188: e in (f ** F) implies ex w st e = (f * w) & w in F

    proof

      (f ** F) = { (f * w) : w in F } by Th187;

      hence thesis;

    end;

    registration

      let F be empty set;

      let f be ExtReal;

      cluster (f ** F) -> empty;

      coherence ;

    end

    registration

      let F be ext-real-membered non empty set;

      let f be ExtReal;

      cluster (f ** F) -> non empty;

      coherence ;

    end

    registration

      let F be ext-real-membered set;

      let f be ExtReal;

      cluster (f ** F) -> ext-real-membered;

      coherence ;

    end

    theorem :: MEMBER_1:189

    r <> 0 implies (r ** (F /\ G)) = ((r ** F) /\ (r ** G))

    proof

      assume

       A1: r <> 0 ;



       A2: ((r ** F) /\ (r ** G)) c= (r ** (F /\ G))

      proof

        let j;

        assume

         A3: j in ((r ** F) /\ (r ** G));

        then j in (r ** F) by XBOOLE_0:def 4;

        then

        consider w such that

         A4: j = (r * w) and

         A5: w in F by Th188;

        j in (r ** G) by A3, XBOOLE_0:def 4;

        then

        consider w1 such that

         A6: j = (r * w1) and

         A7: w1 in G by Th188;

        w = w1 by A1, A4, A6, XXREAL_3: 68;

        then w in (F /\ G) by A5, A7, XBOOLE_0:def 4;

        hence thesis by A4, Th186;

      end;

      (r ** (F /\ G)) c= ((r ** F) /\ (r ** G)) by Th83;

      hence thesis by A2;

    end;

    theorem :: MEMBER_1:190



     Th190: ((f ** F) \ (f ** G)) c= (f ** (F \ G))

    proof

      let i;

      assume

       A1: i in ((f ** F) \ (f ** G));

      then

      consider w such that

       A2: i = (f * w) and

       A3: w in F by Th188;

      now

        assume not w in (F \ G);

        then w in G by A3, XBOOLE_0:def 5;

        then (f * w) in (f ** G) by Th186;

        hence contradiction by A1, A2, XBOOLE_0:def 5;

      end;

      hence thesis by A2, Th186;

    end;

    theorem :: MEMBER_1:191



     Th191: r <> 0 implies (r ** (F \ G)) = ((r ** F) \ (r ** G))

    proof

      assume

       A1: r <> 0 ;



       A2: (r ** (F \ G)) c= ((r ** F) \ (r ** G))

      proof

        let i;

        assume i in (r ** (F \ G));

        then

        consider w such that

         A3: i = (r * w) and

         A4: w in (F \ G) by Th188;

         A5:

        now

          assume (r * w) in (r ** G);

          then

          consider w1 such that

           A6: (r * w) = (r * w1) and

           A7: w1 in G by Th188;

          w = w1 by A1, A6, XXREAL_3: 68;

          hence contradiction by A4, A7, XBOOLE_0:def 5;

        end;

        (r * w) in (r ** F) by A4, Th186;

        hence thesis by A3, A5, XBOOLE_0:def 5;

      end;

      ((r ** F) \ (r ** G)) c= (r ** (F \ G)) by Th190;

      hence thesis by A2;

    end;

    theorem :: MEMBER_1:192

    r <> 0 implies (r ** (F \+\ G)) = ((r ** F) \+\ (r ** G))

    proof

      assume

       A1: r <> 0 ;



      thus (r ** (F \+\ G)) = ((r ** (F \ G)) \/ (r ** (G \ F))) by Th82

      .= (((r ** F) \ (r ** G)) \/ (r ** (G \ F))) by A1, Th191

      .= ((r ** F) \+\ (r ** G)) by A1, Th191;

    end;

    definition

      let A be complex-membered set;

      let a be Complex;

      :: MEMBER_1:def20

      func a ** A -> set equals ( {a} ** A);

      coherence ;

    end

    theorem :: MEMBER_1:193



     Th193: b in A implies (a * b) in (a ** A)

    proof

      a in {a} by TARSKI:def 1;

      hence thesis;

    end;

    theorem :: MEMBER_1:194



     Th194: (a ** A) = { (a * c) : c in A }

    proof

      thus (a ** A) c= { (a * c) : c in A }

      proof

        let e be object;

        assume e in (a ** A);

        then

        consider c1, c2 such that

         A1: e = (c1 * c2) and

         A2: c1 in {a} and

         A3: c2 in A;

        c1 = a by A2, TARSKI:def 1;

        hence thesis by A1, A3;

      end;

      let e be object;

      assume e in { (a * c) : c in A };

      then ex c st e = (a * c) & c in A;

      hence thesis by Th193;

    end;

    theorem :: MEMBER_1:195



     Th195: e in (a ** A) implies ex c st e = (a * c) & c in A

    proof

      (a ** A) = { (a * c) : c in A } by Th194;

      hence thesis;

    end;

    registration

      let A be empty set;

      let a be Complex;

      cluster (a ** A) -> empty;

      coherence ;

    end

    registration

      let A be complex-membered non empty set;

      let a be Complex;

      cluster (a ** A) -> non empty;

      coherence ;

    end

    registration

      let A be complex-membered set;

      let a be Complex;

      cluster (a ** A) -> complex-membered;

      coherence ;

    end

    registration

      let A be real-membered set;

      let a be Real;

      cluster (a ** A) -> real-membered;

      coherence ;

    end

    registration

      let A be rational-membered set;

      let a be Rational;

      cluster (a ** A) -> rational-membered;

      coherence ;

    end

    registration

      let A be integer-membered set;

      let a be Integer;

      cluster (a ** A) -> integer-membered;

      coherence ;

    end

    registration

      let A be natural-membered set;

      let a be Nat;

      cluster (a ** A) -> natural-membered;

      coherence ;

    end

    registration

      let A be real-membered set, F be ext-real-membered set;

      let a be Real, f be ExtReal;

      identify f ** F with a ** A when a = f, A = F;

      compatibility ;

    end

    theorem :: MEMBER_1:196



     Th196: a <> 0 & (a ** A) c= (a ** B) implies A c= B

    proof

      assume that

       A1: a <> 0 and

       A2: (a ** A) c= (a ** B);

      let z;

      assume z in A;

      then (a * z) in (a ** A) by Th193;

      then ex c st (a * z) = (a * c) & c in B by A2, Th195;

      hence thesis by A1, XCMPLX_1: 5;

    end;

    theorem :: MEMBER_1:197

    a <> 0 & (a ** A) = (a ** B) implies A = B

    proof

      assume a <> 0 & (a ** A) = (a ** B);

      then A c= B & B c= A by Th196;

      hence thesis;

    end;

    theorem :: MEMBER_1:198



     Th198: a <> 0 implies (a ** (A /\ B)) = ((a ** A) /\ (a ** B))

    proof

      assume

       A1: a <> 0 ;



       A2: ((a ** A) /\ (a ** B)) c= (a ** (A /\ B))

      proof

        let z;

        assume

         A3: z in ((a ** A) /\ (a ** B));

        then z in (a ** A) by XBOOLE_0:def 4;

        then

        consider c such that

         A4: z = (a * c) and

         A5: c in A by Th195;

        z in (a ** B) by A3, XBOOLE_0:def 4;

        then

        consider c1 such that

         A6: z = (a * c1) and

         A7: c1 in B by Th195;

        c = c1 by A1, A4, A6, XCMPLX_1: 5;

        then c in (A /\ B) by A5, A7, XBOOLE_0:def 4;

        hence thesis by A4, Th193;

      end;

      (a ** (A /\ B)) c= ((a ** A) /\ (a ** B)) by Th93;

      hence thesis by A2;

    end;

    theorem :: MEMBER_1:199



     Th199: a <> 0 implies (a ** (A \ B)) = ((a ** A) \ (a ** B))

    proof

      assume

       A1: a <> 0 ;

      let z;

      hereby

        assume z in (a ** (A \ B));

        then

        consider c such that

         A2: z = (a * c) and

         A3: c in (A \ B) by Th195;

         A4:

        now

          assume (a * c) in (a ** B);

          then

          consider c1 such that

           A5: (a * c) = (a * c1) and

           A6: c1 in B by Th195;

          c = c1 by A1, A5, XCMPLX_1: 5;

          hence contradiction by A3, A6, XBOOLE_0:def 5;

        end;

        (a * c) in (a ** A) by A3, Th193;

        hence z in ((a ** A) \ (a ** B)) by A2, A4, XBOOLE_0:def 5;

      end;

      assume

       A7: z in ((a ** A) \ (a ** B));

      then

      consider c such that

       A8: z = (a * c) and

       A9: c in A by Th195;

      now

        assume not c in (A \ B);

        then c in B by A9, XBOOLE_0:def 5;

        then (a * c) in (a ** B) by Th193;

        hence contradiction by A7, A8, XBOOLE_0:def 5;

      end;

      hence thesis by A8, Th193;

    end;

    theorem :: MEMBER_1:200



     Th200: a <> 0 implies (a ** (A \+\ B)) = ((a ** A) \+\ (a ** B))

    proof

      assume

       A1: a <> 0 ;



      thus (a ** (A \+\ B)) = ((a ** (A \ B)) \/ (a ** (B \ A))) by Th92

      .= (((a ** A) \ (a ** B)) \/ (a ** (B \ A))) by A1, Th199

      .= ((a ** A) \+\ (a ** B)) by A1, Th199;

    end;

    theorem :: MEMBER_1:201



     Th201: ( 0 ** A) c= { 0 }

    proof

      let a;

      assume a in ( 0 ** A);

      then

      consider c1, c2 such that

       A1: a = (c1 * c2) and

       A2: c1 in { 0 } and c2 in A;

      c1 = 0 by A2, TARSKI:def 1;

      hence thesis by A1, TARSKI:def 1;

    end;

    theorem :: MEMBER_1:202

    A <> {} implies ( 0 ** A) = { 0 }

    proof

      assume

       A1: A <> {} ;



       A2: { 0 } c= ( 0 ** A)

      proof

        set x = the Element of A;

        let a be Nat;

        assume

         A3: a in { 0 };



         A4: ( 0 * x) in { ( 0 * c) : c in A } by A1;

        ( 0 ** A) = { ( 0 * c) : c in A } by Th194;

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

      end;

      ( 0 ** A) c= { 0 } by Th201;

      hence thesis by A2;

    end;

    theorem :: MEMBER_1:203

    (1 ** A) = A

    proof

      let a;

      hereby

        assume a in (1 ** A);

        then

        consider c1, c2 such that

         A1: a = (c1 * c2) and

         A2: c1 in {1} and

         A3: c2 in A;

        c1 = 1 by A2, TARSKI:def 1;

        hence a in A by A1, A3;

      end;

      assume a in A;

      then (1 * a) in { (1 * c) : c in A };

      hence thesis by Th194;

    end;

    theorem :: MEMBER_1:204

    ((a * b) ** A) = (a ** (b ** A))

    proof



      thus ((a * b) ** A) = (( {a} ** {b}) ** A) by Th98

      .= (a ** (b ** A)) by Th90;

    end;

    theorem :: MEMBER_1:205

    (a ** (A ** B)) = ((a ** A) ** B) by Th90;

    theorem :: MEMBER_1:206

    ((a + b) ** A) c= ((a ** A) ++ (b ** A))

    proof

      ( {a} ++ {b}) = {(a + b)} by Th51;

      hence thesis by Th95;

    end;

    theorem :: MEMBER_1:207

    ((a - b) ** A) c= ((a ** A) -- (b ** A))

    proof

      ( {a} -- {b}) = {(a - b)} by Th75;

      hence thesis by Th96;

    end;

    theorem :: MEMBER_1:208



     Th208: (a ** (B ++ C)) = ((a ** B) ++ (a ** C))

    proof



       A1: ((a ** B) ++ (a ** C)) c= (a ** (B ++ C))

      proof

        let z;

        assume z in ((a ** B) ++ (a ** C));

        then

        consider c, c1 such that

         A2: z = (c + c1) and

         A3: c in (a ** B) and

         A4: c1 in (a ** C);

        consider c3 be Complex such that

         A5: c1 = (a * c3) and

         A6: c3 in C by A4, Th195;

        consider c2 such that

         A7: c = (a * c2) and

         A8: c2 in B by A3, Th195;



         A9: (c2 + c3) in (B ++ C) by A8, A6;

        z = (a * (c2 + c3)) by A2, A7, A5;

        hence thesis by A9, Th193;

      end;

      (a ** (B ++ C)) c= ((a ** B) ++ (a ** C)) by Th95;

      hence thesis by A1;

    end;

    theorem :: MEMBER_1:209

    (a ** (B -- C)) = ((a ** B) -- (a ** C))

    proof



      thus (a ** (B -- C)) = ((a ** B) ++ (a ** ( -- C))) by Th208

      .= ((a ** B) -- (a ** C)) by Th94;

    end;

    definition

      let F be ext-real-membered set;

      let f be ExtReal;

      :: MEMBER_1:def21

      func f /// F -> set equals ( {f} /// F);

      coherence ;

    end

    theorem :: MEMBER_1:210



     Th210: g in G implies (f / g) in (f /// G)

    proof

      f in {f} by TARSKI:def 1;

      hence thesis by Th102;

    end;

    theorem :: MEMBER_1:211



     Th211: (f /// F) = { (f / w) : w in F }

    proof

      thus (f /// F) c= { (f / w) : w in F }

      proof

        let e be object;

        assume e in (f /// F);

        then

        consider w1, w2 such that

         A1: e = (w1 * w2) and

         A2: w1 in {f} and

         A3: w2 in (F "" );

        consider w3 be Element of ExtREAL such that

         A4: w2 = (w3 " ) & w3 in F by A3;

        (w1 * (w3 " )) = (w1 / w3) & w1 = f by A2, TARSKI:def 1;

        hence thesis by A1, A4;

      end;

      let e be object;

      assume e in { (f / w) : w in F };

      then ex w st e = (f / w) & w in F;

      hence thesis by Th210;

    end;

    theorem :: MEMBER_1:212

    e in (f /// F) implies ex w st e = (f / w) & w in F

    proof

      (f /// F) = { (f / w) : w in F } by Th211;

      hence thesis;

    end;

    registration

      let F be empty set;

      let f be ExtReal;

      cluster (f /// F) -> empty;

      coherence ;

    end

    registration

      let F be ext-real-membered non empty set;

      let f be ExtReal;

      cluster (f /// F) -> non empty;

      coherence ;

    end

    registration

      let F be ext-real-membered set;

      let f be ExtReal;

      cluster (f /// F) -> ext-real-membered;

      coherence ;

    end

    definition

      let A be complex-membered set;

      let a be Complex;

      :: MEMBER_1:def22

      func a /// A -> set equals ( {a} /// A);

      coherence ;

    end

    theorem :: MEMBER_1:213



     Th213: b in A implies (a / b) in (a /// A)

    proof

      a in {a} by TARSKI:def 1;

      hence thesis by Th116;

    end;

    theorem :: MEMBER_1:214



     Th214: (a /// A) = { (a / c) : c in A }

    proof

      thus (a /// A) c= { (a / c) : c in A }

      proof

        let e be object;

        assume e in (a /// A);

        then

        consider c1, c2 such that

         A1: e = (c1 * c2) and

         A2: c1 in {a} & c2 in (A "" );



         A3: (c1 * c2) = (c1 / (c2 " ));

        (c2 " ) in A & c1 = a by A2, Th29, TARSKI:def 1;

        hence thesis by A1, A3;

      end;

      let e be object;

      assume e in { (a / c) : c in A };

      then ex c st e = (a / c) & c in A;

      hence thesis by Th213;

    end;

    theorem :: MEMBER_1:215



     Th215: e in (a /// A) implies ex c st e = (a / c) & c in A

    proof

      (a /// A) = { (a / c) : c in A } by Th214;

      hence thesis;

    end;

    registration

      let A be empty set;

      let a be Complex;

      cluster (a /// A) -> empty;

      coherence ;

    end

    registration

      let A be complex-membered non empty set;

      let a be Complex;

      cluster (a /// A) -> non empty;

      coherence ;

    end

    registration

      let A be complex-membered set;

      let a be Complex;

      cluster (a /// A) -> complex-membered;

      coherence ;

    end

    registration

      let A be real-membered set;

      let a be Real;

      cluster (a /// A) -> real-membered;

      coherence ;

    end

    registration

      let A be rational-membered set;

      let a be Rational;

      cluster (a /// A) -> rational-membered;

      coherence ;

    end

    registration

      let A be real-membered set, F be ext-real-membered set;

      let a be Real, f be ExtReal;

      identify f /// F with a /// A when a = f, A = F;

      compatibility ;

    end

    theorem :: MEMBER_1:216



     Th216: a <> 0 & (a /// A) c= (a /// B) implies A c= B

    proof

      assume that

       A1: a <> 0 and

       A2: (a /// A) c= (a /// B);

      let z;

      assume z in A;

      then (a / z) in (a /// A) by Th213;

      then

      consider c such that

       A3: (a / z) = (a / c) and

       A4: c in B by A2, Th215;

      (z " ) = (c " ) by A1, A3, XCMPLX_1: 5;

      hence thesis by A4, XCMPLX_1: 201;

    end;

    theorem :: MEMBER_1:217

    a <> 0 & (a /// A) = (a /// B) implies A = B

    proof

      assume a <> 0 & (a /// A) = (a /// B);

      then A c= B & B c= A by Th216;

      hence thesis;

    end;

    theorem :: MEMBER_1:218

    a <> 0 implies (a /// (A /\ B)) = ((a /// A) /\ (a /// B))

    proof

      assume

       A1: a <> 0 ;



      thus (a /// (A /\ B)) = (a ** ((A "" ) /\ (B "" ))) by Th33

      .= ((a ** (A "" )) /\ (a ** (B "" ))) by A1, Th198

      .= ((a /// A) /\ (a /// B));

    end;

    theorem :: MEMBER_1:219

    a <> 0 implies (a /// (A \ B)) = ((a /// A) \ (a /// B))

    proof

      assume

       A1: a <> 0 ;



      thus (a /// (A \ B)) = (a ** ((A "" ) \ (B "" ))) by Th34

      .= ((a ** (A "" )) \ (a ** (B "" ))) by A1, Th199

      .= ((a /// A) \ (a /// B));

    end;

    theorem :: MEMBER_1:220

    a <> 0 implies (a /// (A \+\ B)) = ((a /// A) \+\ (a /// B))

    proof

      assume

       A1: a <> 0 ;



      thus (a /// (A \+\ B)) = (a ** ((A "" ) \+\ (B "" ))) by Th35

      .= ((a ** (A "" )) \+\ (a ** (B "" ))) by A1, Th200

      .= ((a /// A) \+\ (a /// B));

    end;

    theorem :: MEMBER_1:221

    ((a + b) /// A) c= ((a /// A) ++ (b /// A))

    proof

      ( {a} ++ {b}) = {(a + b)} by Th51;

      hence thesis by Th95;

    end;

    theorem :: MEMBER_1:222

    ((a - b) /// A) c= ((a /// A) -- (b /// A))

    proof

      ( {a} -- {b}) = {(a - b)} by Th75;

      hence thesis by Th96;

    end;

    definition

      let F be ext-real-membered set;

      let f be ExtReal;

      :: MEMBER_1:def23

      func F /// f -> set equals (F /// {f});

      coherence ;

    end

    theorem :: MEMBER_1:223



     Th223: g in G implies (g / f) in (G /// f)

    proof

      f in {f} by TARSKI:def 1;

      hence thesis by Th102;

    end;

    theorem :: MEMBER_1:224



     Th224: (F /// f) = { (w / f) : w in F }

    proof

      thus (F /// f) c= { (w / f) : w in F }

      proof

        let e be object;

        assume e in (F /// f);

        then

        consider w1, w2 such that

         A1: e = (w1 * w2) & w1 in F and

         A2: w2 in ( {f} "" );

        consider w3 be Element of ExtREAL such that

         A3: w2 = (w3 " ) and

         A4: w3 in {f} by A2;

        (w1 * (w3 " )) = (w1 / w3) & w3 = f by A4, TARSKI:def 1;

        hence thesis by A1, A3;

      end;

      let e be object;

      assume e in { (w / f) : w in F };

      then ex w st e = (w / f) & w in F;

      hence thesis by Th223;

    end;

    theorem :: MEMBER_1:225

    e in (F /// f) implies ex w st e = (w / f) & w in F

    proof

      (F /// f) = { (w / f) : w in F } by Th224;

      hence thesis;

    end;

    registration

      let F be empty set;

      let f be ExtReal;

      cluster (F /// f) -> empty;

      coherence ;

    end

    registration

      let F be ext-real-membered non empty set;

      let f be ExtReal;

      cluster (F /// f) -> non empty;

      coherence ;

    end

    registration

      let F be ext-real-membered set;

      let f be ExtReal;

      cluster (F /// f) -> ext-real-membered;

      coherence ;

    end

    definition

      let A be complex-membered set;

      let a be Complex;

      :: MEMBER_1:def24

      func A /// a -> set equals (A /// {a});

      coherence ;

    end

    theorem :: MEMBER_1:226



     Th226: b in A implies (b / a) in (A /// a)

    proof

      a in {a} by TARSKI:def 1;

      hence thesis by Th116;

    end;

    theorem :: MEMBER_1:227



     Th227: (A /// a) = { (c / a) : c in A }

    proof

      thus (A /// a) c= { (c / a) : c in A }

      proof

        let e be object;

        assume e in (A /// a);

        then

        consider c1, c2 such that

         A1: e = (c1 * c2) & c1 in A and

         A2: c2 in ( {a} "" );

        ( {a} "" ) = {(a " )} by Th37;

        then (c1 * c2) = (c1 / (c2 " )) & c2 = (a " ) by A2, TARSKI:def 1;

        hence thesis by A1;

      end;

      let e be object;

      assume e in { (c / a) : c in A };

      then ex c st e = (c / a) & c in A;

      hence thesis by Th226;

    end;

    theorem :: MEMBER_1:228



     Th228: e in (A /// a) implies ex c st e = (c / a) & c in A

    proof

      (A /// a) = { (c / a) : c in A } by Th227;

      hence thesis;

    end;

    registration

      let A be empty set;

      let a be Complex;

      cluster (A /// a) -> empty;

      coherence ;

    end

    registration

      let A be complex-membered non empty set;

      let a be Complex;

      cluster (A /// a) -> non empty;

      coherence ;

    end

    registration

      let A be complex-membered set;

      let a be Complex;

      cluster (A /// a) -> complex-membered;

      coherence ;

    end

    registration

      let A be real-membered set;

      let a be Real;

      cluster (A /// a) -> real-membered;

      coherence ;

    end

    registration

      let A be rational-membered set;

      let a be Rational;

      cluster (A /// a) -> rational-membered;

      coherence ;

    end

    registration

      let A be real-membered set, F be ext-real-membered set;

      let a be Real, f be ExtReal;

      identify F /// f with A /// a when a = f, A = F;

      compatibility ;

    end

    theorem :: MEMBER_1:229



     Th229: a <> 0 & (A /// a) c= (B /// a) implies A c= B

    proof

      assume that

       A1: a <> 0 and

       A2: (A /// a) c= (B /// a);

      let z;

      assume z in A;

      then (z / a) in (A /// a) by Th226;

      then ex c st (z / a) = (c / a) & c in B by A2, Th228;

      hence thesis by A1, XCMPLX_1: 5;

    end;

    theorem :: MEMBER_1:230

    a <> 0 & (A /// a) = (B /// a) implies A = B

    proof

      assume a <> 0 & (A /// a) = (B /// a);

      then A c= B & B c= A by Th229;

      hence thesis;

    end;

    theorem :: MEMBER_1:231

    a <> 0 implies ((A /\ B) /// a) = ((A /// a) /\ (B /// a))

    proof

      assume

       A1: a <> 0 ;



       A2: ( {a} "" ) = {(a " )} by Th37;



      thus ((A /\ B) /// a) = ((a " ) ** (A /\ B)) by Th37

      .= (((a " ) ** A) /\ ((a " ) ** B)) by A1, Th198

      .= ((A /// a) /\ (B /// a)) by A2;

    end;

    theorem :: MEMBER_1:232

    a <> 0 implies ((A \ B) /// a) = ((A /// a) \ (B /// a))

    proof

      assume

       A1: a <> 0 ;



       A2: ( {a} "" ) = {(a " )} by Th37;



      thus ((A \ B) /// a) = ((a " ) ** (A \ B)) by Th37

      .= (((a " ) ** A) \ ((a " ) ** B)) by A1, Th199

      .= ((A /// a) \ (B /// a)) by A2;

    end;

    theorem :: MEMBER_1:233

    a <> 0 implies ((A \+\ B) /// a) = ((A /// a) \+\ (B /// a))

    proof

      assume

       A1: a <> 0 ;



       A2: ( {a} "" ) = {(a " )} by Th37;



      thus ((A \+\ B) /// a) = ((a " ) ** (A \+\ B)) by Th37

      .= (((a " ) ** A) \+\ ((a " ) ** B)) by A1, Th200

      .= ((A /// a) \+\ (B /// a)) by A2;

    end;

    theorem :: MEMBER_1:234



     Th234: ((A ++ B) /// a) = ((A /// a) ++ (B /// a))

    proof



      thus ((A ++ B) /// a) = ((a " ) ** (A ++ B)) by Th37

      .= (((a " ) ** A) ++ ((a " ) ** B)) by Th208

      .= ((A /// a) ++ ((a " ) ** B)) by Th37

      .= ((A /// a) ++ (B /// a)) by Th37;

    end;

    theorem :: MEMBER_1:235

    ((A -- B) /// a) = ((A /// a) -- (B /// a))

    proof



      thus ((A -- B) /// a) = ((A /// a) ++ (( -- B) /// a)) by Th234

      .= ((A /// a) -- (B /// a)) by Th94;

    end;