struct_0.miz

    begin

    definition

      struct 1-sorted (# the carrier -> set #)

       attr strict strict;

    end

    definition

      let S be 1-sorted;

      :: STRUCT_0:def1

      attr S is empty means

      : Def1: the carrier of S is empty;

    end

    registration

      cluster strict empty for 1-sorted;

      existence

      proof

        take T = 1-sorted (# {} #);

        thus T is strict;

        thus the carrier of T is empty;

      end;

    end

    registration

      cluster strict non empty for 1-sorted;

      existence

      proof

        take 1-sorted (# { {} } #);

        thus 1-sorted (# { {} } #) is strict;

        thus the carrier of 1-sorted (# { {} } #) is non empty;

      end;

    end

    registration

      let S be empty 1-sorted;

      cluster the carrier of S -> empty;

      coherence by Def1;

    end

    registration

      let S be non empty 1-sorted;

      cluster the carrier of S -> non empty;

      coherence by Def1;

    end

    definition

      let S be 1-sorted;

      mode Element of S is Element of the carrier of S;

      mode Subset of S is Subset of the carrier of S;

      mode Subset-Family of S is Subset-Family of the carrier of S;

    end

    definition

      let S be 1-sorted, X be set;

      mode Function of S,X is Function of the carrier of S, X;

      mode Function of X,S is Function of X, the carrier of S;

    end

    definition

      let S,T be 1-sorted;

      mode Function of S,T is Function of the carrier of S, the carrier of T;

    end

    definition

      let T be 1-sorted;

      :: STRUCT_0:def2

      func {} T -> Subset of T equals {} ;

      coherence

      proof

         {} = ( {} the carrier of T);

        hence thesis;

      end;

      :: STRUCT_0:def3

      func [#] T -> Subset of T equals the carrier of T;

      coherence

      proof

        the carrier of T = ( [#] the carrier of T);

        hence thesis;

      end;

    end

    registration

      let T be 1-sorted;

      cluster ( {} T) -> empty;

      coherence ;

    end

    registration

      let T be empty 1-sorted;

      cluster ( [#] T) -> empty;

      coherence ;

    end

    registration

      let T be non empty 1-sorted;

      cluster ( [#] T) -> non empty;

      coherence ;

    end

    registration

      let S be non empty 1-sorted;

      cluster non empty for Subset of S;

      existence

      proof

        take ( [#] S);

        thus thesis;

      end;

    end

    definition

      let S be 1-sorted;

      mode FinSequence of S is FinSequence of the carrier of S;

    end

    definition

      let S be 1-sorted;

      mode ManySortedSet of S is ManySortedSet of the carrier of S;

    end

    definition

      let S be 1-sorted;

      :: STRUCT_0:def4

      func id S -> Function of S, S equals ( id the carrier of S);

      coherence ;

    end

    definition

      let S be 1-sorted;

      mode sequence of S is sequence of the carrier of S;

    end

    definition

      let S be 1-sorted, X be set;

      mode PartFunc of S,X is PartFunc of the carrier of S, X;

      mode PartFunc of X,S is PartFunc of X, the carrier of S;

    end

    definition

      let S,T be 1-sorted;

      mode PartFunc of S,T is PartFunc of the carrier of S, the carrier of T;

    end

    definition

      let S be 1-sorted;

      let x be object;

      :: STRUCT_0:def5

      pred x in S means x in the carrier of S;

    end

    definition

      struct ( 1-sorted) ZeroStr (# the carrier -> set,

the ZeroF -> Element of the carrier #)

       attr strict strict;

    end

    registration

      cluster strict non empty for ZeroStr;

      existence

      proof

        set A = the non empty set, a = the Element of A;

        take ZeroStr (# A, a #);

        thus ZeroStr (# A, a #) is strict;

        thus the carrier of ZeroStr (# A, a #) is non empty;

      end;

    end

    definition

      struct ( 1-sorted) OneStr (# the carrier -> set,

the OneF -> Element of the carrier #)

       attr strict strict;

    end

    definition

      struct ( ZeroStr, OneStr) ZeroOneStr (# the carrier -> set,

the ZeroF -> Element of the carrier,

the OneF -> Element of the carrier #)

       attr strict strict;

    end

    definition

      let S be ZeroStr;

      :: STRUCT_0:def6

      func 0. S -> Element of S equals the ZeroF of S;

      coherence ;

    end

    definition

      let S be OneStr;

      :: STRUCT_0:def7

      func 1. S -> Element of S equals the OneF of S;

      coherence ;

    end

    definition

      let S be ZeroOneStr;

      :: STRUCT_0:def8

      attr S is degenerated means

      : Def8: ( 0. S) = ( 1. S);

    end

    definition

      let IT be 1-sorted;

      :: STRUCT_0:def9

      attr IT is trivial means

      : Def9: the carrier of IT is trivial;

    end

    registration

      cluster empty -> trivial for 1-sorted;

      coherence ;

      cluster non trivial -> non empty for 1-sorted;

      coherence ;

    end

    definition

      let S be 1-sorted;

      :: original: trivial

      redefine

      :: STRUCT_0:def10

      attr S is trivial means

      : Def10: for x,y be Element of S holds x = y;

      compatibility

      proof

        set I = the carrier of S;

        per cases ;

          suppose I is non empty;

          thus S is trivial implies for x,y be Element of I holds x = y

          proof

            assume

             A2: I is trivial;

            let x,y be Element of I;

            thus thesis by A2;

          end;

          assume

           A3: for x,y be Element of I holds x = y;

          let x,y be object;

          thus thesis by A3;

        end;

          suppose

           A4: I is empty;

          for x,y be Element of I holds x = y

          proof

            let x,y be Element of I;



            thus x = {} by A4, SUBSET_1:def 1

            .= y by A4, SUBSET_1:def 1;

          end;

          hence thesis by A4;

        end;

      end;

    end

    registration

      cluster non degenerated -> non trivial for ZeroOneStr;

      coherence ;

    end

    registration

      cluster trivial non empty strict for 1-sorted;

      existence

      proof

        take 1-sorted (# 1 #);

        thus thesis by CARD_1: 49;

      end;

      cluster non trivial strict for 1-sorted;

      existence

      proof

        take Y = 1-sorted (# 2 #);

        reconsider x = 0 , y = 1 as Element of Y by CARD_1: 50, TARSKI:def 2;

        x <> y;

        hence thesis;

      end;

    end

    registration

      let S be non trivial 1-sorted;

      cluster the carrier of S -> non trivial;

      coherence by Def9;

    end

    registration

      let S be trivial 1-sorted;

      cluster the carrier of S -> trivial;

      coherence by Def9;

    end

    begin

    definition

      let S be 1-sorted;

      :: STRUCT_0:def11

      attr S is finite means

      : Def11: the carrier of S is finite;

    end

    registration

      cluster strict finite non empty for 1-sorted;

      existence

      proof

        take 1-sorted (# { {} } #);

        thus thesis;

      end;

    end

    registration

      let S be finite 1-sorted;

      cluster the carrier of S -> finite;

      coherence by Def11;

    end

    registration

      cluster -> finite for empty 1-sorted;

      coherence ;

    end

    notation

      let S be 1-sorted;

      antonym S is infinite for S is finite;

    end

    registration

      cluster strict infinite for 1-sorted;

      existence

      proof

        take A = 1-sorted (# the infinite set #);

        thus A is strict;

        thus the carrier of A is infinite;

      end;

    end

    registration

      let S be infinite 1-sorted;

      cluster the carrier of S -> infinite;

      coherence by Def11;

    end

    registration

      cluster -> non empty for infinite 1-sorted;

      coherence ;

    end

    registration

      cluster trivial -> finite for 1-sorted;

      coherence ;

    end

    registration

      cluster infinite -> non trivial for 1-sorted;

      coherence ;

    end

    definition

      let S be ZeroStr, x be Element of S;

      :: STRUCT_0:def12

      attr x is zero means x = ( 0. S);

    end

    registration

      let S be ZeroStr;

      cluster ( 0. S) -> zero;

      coherence ;

    end

    registration

      cluster strict non degenerated for ZeroOneStr;

      existence

      proof

        take S = ZeroOneStr (# 2, ( In ( 0 ,2)), ( In (1,2)) #);

         0 in 2 by CARD_1: 50, TARSKI:def 2;

        then 1 in 2 & ( In ( 0 ,2)) = 0 by CARD_1: 50, SUBSET_1:def 8, TARSKI:def 2;

        then ( 0. S) <> ( 1. S) by SUBSET_1:def 8;

        hence thesis;

      end;

    end

    registration

      let S be non degenerated ZeroOneStr;

      cluster ( 1. S) -> non zero;

      coherence by Def8;

    end

    definition

      let S be 1-sorted;

      mode Cover of S is Cover of the carrier of S;

    end

    registration

      let S be 1-sorted;

      cluster ( [#] S) -> non proper;

      coherence ;

    end

    begin

    definition

      struct ( 1-sorted) 2-sorted (# the carrier, carrier' -> set #)

       attr strict strict;

    end

    definition

      let S be 2-sorted;

      :: STRUCT_0:def13

      attr S is void means

      : Def13: the carrier' of S is empty;

    end

    registration

      cluster strict empty void for 2-sorted;

      existence

      proof

        take S = 2-sorted (# {} , {} #);

        thus S is strict;

        thus the carrier of S is empty;

        thus the carrier' of S is empty;

      end;

    end

    registration

      let S be void 2-sorted;

      cluster the carrier' of S -> empty;

      coherence by Def13;

    end

    registration

      cluster strict non empty non void for 2-sorted;

      existence

      proof

        take S = 2-sorted (# { 0 }, { 0 } #);

        thus S is strict;

        thus not the carrier of S is empty;

        thus not the carrier' of S is empty;

      end;

    end

    registration

      let S be non void 2-sorted;

      cluster the carrier' of S -> non empty;

      coherence by Def13;

    end

    definition

      let X be 1-sorted, Y be non empty 1-sorted, y be Element of Y;

      :: STRUCT_0:def14

      func X --> y -> Function of X, Y equals (the carrier of X --> y);

      coherence ;

    end

    registration

      let S be ZeroStr;

      cluster zero for Element of S;

      existence

      proof

        take ( 0. S);

        thus ( 0. S) = ( 0. S);

      end;

    end

    registration

      cluster strict non trivial for ZeroStr;

      existence

      proof

        take ZeroStr (# 2, ( In ( 0 ,2)) #);

         0 in 2 & 1 in 2 by CARD_1: 50, TARSKI:def 2;

        hence thesis;

      end;

    end

    registration

      let S be non trivial ZeroStr;

      cluster non zero for Element of S;

      existence

      proof

        consider x,y be Element of S such that

         A1: x <> y by Def10;

        per cases by A1;

          suppose

           A2: x <> ( 0. S);

          take x;

          thus x <> ( 0. S) by A2;

        end;

          suppose

           A3: y <> ( 0. S);

          take y;

          thus y <> ( 0. S) by A3;

        end;

      end;

    end

    definition

      let X be set, S be ZeroStr, R be Relation of X, the carrier of S;

      :: STRUCT_0:def15

      attr R is non-zero means not ( 0. S) in ( rng R);

    end

    definition

      let S be 1-sorted;

      :: STRUCT_0:def16

      func card S -> Cardinal equals ( card the carrier of S);

      coherence ;

    end

    definition

      let S be 1-sorted;

      mode UnOp of S is UnOp of the carrier of S;

      mode BinOp of S is BinOp of the carrier of S;

    end

    definition

      let S be ZeroStr;

      :: STRUCT_0:def17

      func NonZero S -> Subset of S equals (( [#] S) \ {( 0. S)});

      coherence ;

    end

    theorem :: STRUCT_0:1

    for S be non empty ZeroStr holds for u be Element of S holds u in ( NonZero S) iff not u is zero by ZFMISC_1: 56;

    definition

      let V be non empty ZeroStr;

      :: original: trivial

      redefine

      :: STRUCT_0:def18

      attr V is trivial means

      : Def18: for u be Element of V holds u = ( 0. V);

      compatibility

      proof

        thus V is trivial implies for a be Element of V holds a = ( 0. V);

        assume

         A1: for a be Element of V holds a = ( 0. V);

        let a,b be Element of V;



        thus a = ( 0. V) by A1

        .= b by A1;

      end;

    end

    registration

      let V be non trivial ZeroStr;

      cluster ( NonZero V) -> non empty;

      coherence

      proof

        ex u be Element of V st u <> ( 0. V) by Def18;

        hence thesis by ZFMISC_1: 56;

      end;

    end

    registration

      cluster trivial non empty for ZeroStr;

      existence

      proof

        take ZeroStr (# 1, ( In ( 0 ,1)) #);

        thus thesis by CARD_1: 49;

      end;

    end

    registration

      let S be trivial non empty ZeroStr;

      cluster ( NonZero S) -> empty;

      coherence

      proof

        assume not ( NonZero S) is empty;

        then

        consider x be Element of S such that

         A1: x in ( NonZero S) by SUBSET_1: 4;

         not x in {( 0. S)} by A1, XBOOLE_0:def 5;

        then x <> ( 0. S) by TARSKI:def 1;

        hence contradiction by Def18;

      end;

    end

    registration

      let S be non empty 1-sorted;

      cluster non empty trivial for Subset of S;

      existence

      proof

         { the Element of S} is Subset of S;

        hence thesis;

      end;

    end

    theorem :: STRUCT_0:2

    for F be non degenerated ZeroOneStr holds ( 1. F) in ( NonZero F)

    proof

      let F be non degenerated ZeroOneStr;

       not ( 1. F) in {( 0. F)} by TARSKI:def 1;

      hence thesis by XBOOLE_0:def 5;

    end;

    registration

      let S be finite 1-sorted;

      cluster ( card S) -> natural;

      coherence ;

    end

    registration

      let S be finite non empty 1-sorted;

      cluster ( card S) -> non zero;

      coherence ;

    end

    registration

      let T be non trivial 1-sorted;

      cluster non trivial for Subset of T;

      existence

      proof

        consider x,y be Element of T such that

         A1: x <> y by Def10;

        reconsider A = {x, y} as Subset of T;

        take A, x, y;

        thus x in A by TARSKI:def 2;

        thus y in A by TARSKI:def 2;

        thus thesis by A1;

      end;

    end

    theorem :: STRUCT_0:3

    for S be ZeroStr holds not ( 0. S) in ( NonZero S)

    proof

      let S be ZeroStr;

      assume ( 0. S) in ( NonZero S);

      then not ( 0. S) in {( 0. S)} by XBOOLE_0:def 5;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: STRUCT_0:4

    for S be non empty ZeroStr holds the carrier of S = ( {( 0. S)} \/ ( NonZero S)) by XBOOLE_1: 45;

    definition

      let C be set, X be 1-sorted;

      :: STRUCT_0:def19

      attr X is C -element means

      : Def19: the carrier of X is C -element;

    end

    registration

      let C be Cardinal;

      cluster C -element for 1-sorted;

      existence

      proof

        take X = 1-sorted (# the C -element set #);

        thus the carrier of X is C -element;

      end;

    end

    registration

      let C be Cardinal, X be C -element 1-sorted;

      cluster the carrier of X -> C -element;

      coherence by Def19;

    end

    registration

      cluster empty -> 0 -element for 1-sorted;

      coherence ;

      cluster 0 -element -> empty for 1-sorted;

      coherence ;

      cluster non empty trivial -> 1 -element for 1-sorted;

      coherence ;

      cluster 1 -element -> non empty trivial for 1-sorted;

      coherence ;

    end

    definition

      let S be 2-sorted;

      :: STRUCT_0:def20

      attr S is feasible means the carrier of S is empty implies the carrier' of S is empty;

    end

    registration

      cluster non empty -> feasible for 2-sorted;

      coherence ;

      cluster void -> feasible for 2-sorted;

      coherence ;

      cluster empty feasible -> void for 2-sorted;

      coherence ;

      cluster non void feasible -> non empty for 2-sorted;

      coherence ;

    end

    definition

      let S be 2-sorted;

      :: STRUCT_0:def21

      attr S is trivial' means

      : Def21: the carrier' of S is trivial;

    end

    registration

      cluster strict non empty non void trivial trivial' for 2-sorted;

      existence

      proof

        take S = 2-sorted (# { 0 }, { 0 } #);

        thus S is strict;

        thus not S is empty;

        thus not S is void;

        thus S is trivial;

        thus the carrier' of S is trivial;

      end;

    end

    registration

      let S be trivial' 2-sorted;

      cluster the carrier' of S -> trivial;

      coherence by Def21;

    end

    registration

      cluster non trivial' for 2-sorted;

      existence

      proof

        take S = 2-sorted (# 1, { 0 , 1} #);

         0 in { 0 , 1} & 1 in { 0 , 1} by TARSKI:def 2;

        hence thesis by ZFMISC_1:def 10;

      end;

    end

    registration

      let S be non trivial' 2-sorted;

      cluster the carrier' of S -> non trivial;

      coherence by Def21;

    end

    registration

      cluster void -> trivial' for 2-sorted;

      coherence ;

      cluster non trivial -> non empty for 1-sorted;

      coherence ;

    end

    definition

      let x be object, S be 1-sorted;

      :: STRUCT_0:def22

      func In (x,S) -> Element of S equals ( In (x,the carrier of S));

      coherence ;

    end