:: by Library Committee

::

:: Received January 6, 1995

:: Copyright (c) 1995 Association of Mizar Users

begin

definition

attr c_{1} is strict ;

struct 1-sorted -> ;

aggr 1-sorted(# carrier #) -> 1-sorted ;

sel carrier c_{1} -> set ;

end;
struct 1-sorted -> ;

aggr 1-sorted(# carrier #) -> 1-sorted ;

sel carrier c

definition
end;

:: deftheorem Def1 defines empty STRUCT_0:def 1 :

for S being 1-sorted holds

( S is empty iff the carrier of S is empty );

registration

cluster strict empty 1-sorted ;

existence

ex b_{1} being 1-sorted st

( b_{1} is strict & b_{1} is empty )

end;
existence

ex b

( b

proof end;

registration

cluster strict non empty 1-sorted ;

existence

ex b_{1} being 1-sorted st

( b_{1} is strict & not b_{1} is empty )

end;
existence

ex b

( b

proof end;

registration

let S be empty 1-sorted ;

cluster the carrier of S -> empty ;

coherence

the carrier of S is empty by Def1;

end;
cluster the carrier of S -> empty ;

coherence

the carrier of S is empty by Def1;

registration

let S be non empty 1-sorted ;

cluster the carrier of S -> non empty ;

coherence

not the carrier of S is empty by Def1;

end;
cluster the carrier of S -> non empty ;

coherence

not the carrier of S is empty by Def1;

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

definition

let S be 1-sorted ;

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

definition
end;

definition

let T be 1-sorted ;

func {} T -> Subset of T equals :: STRUCT_0:def 2

{} ;

coherence

{} is Subset of T

the carrier of T;

coherence

the carrier of T is Subset of T

end;
func {} T -> Subset of T equals :: STRUCT_0:def 2

{} ;

coherence

{} is Subset of T

proof end;

func [#] T -> Subset of T equals :: STRUCT_0:def 3the carrier of T;

coherence

the carrier of T is Subset of T

proof end;

:: deftheorem defines {} STRUCT_0:def 2 :

for T being 1-sorted holds {} T = {} ;

:: deftheorem defines [#] STRUCT_0:def 3 :

for T being 1-sorted holds [#] T = the carrier of T;

registration
end;

registration

let S be non empty 1-sorted ;

cluster non empty Element of K21( the carrier of S);

existence

not for b_{1} being Subset of S holds b_{1} is empty

end;
cluster non empty Element of K21( the carrier of S);

existence

not for b

proof end;

definition

let S be 1-sorted ;

func id S -> Function of S,S equals :: STRUCT_0:def 4

id the carrier of S;

coherence

id the carrier of S is Function of S,S ;

end;
func id S -> Function of S,S equals :: STRUCT_0:def 4

id the carrier of S;

coherence

id the carrier of S is Function of S,S ;

:: deftheorem defines id STRUCT_0:def 4 :

for S being 1-sorted holds id S = id the carrier of S;

definition

let S be 1-sorted ;

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

definition
end;

definition
end;

:: deftheorem defines in STRUCT_0:def 5 :

for S being 1-sorted

for x being set holds

( x in S iff x in the carrier of S );

definition

attr c_{1} is strict ;

struct ZeroStr -> 1-sorted ;

aggr ZeroStr(# carrier, ZeroF #) -> ZeroStr ;

sel ZeroF c_{1} -> Element of the carrier of c_{1};

end;
struct ZeroStr -> 1-sorted ;

aggr ZeroStr(# carrier, ZeroF #) -> ZeroStr ;

sel ZeroF c

registration

cluster non empty strict ZeroStr ;

existence

ex b_{1} being ZeroStr st

( b_{1} is strict & not b_{1} is empty )

end;
existence

ex b

( b

proof end;

definition

attr c_{1} is strict ;

struct OneStr -> 1-sorted ;

aggr OneStr(# carrier, OneF #) -> OneStr ;

sel OneF c_{1} -> Element of the carrier of c_{1};

end;
struct OneStr -> 1-sorted ;

aggr OneStr(# carrier, OneF #) -> OneStr ;

sel OneF c

definition

attr c_{1} is strict ;

struct ZeroOneStr -> ZeroStr , OneStr ;

aggr ZeroOneStr(# carrier, ZeroF, OneF #) -> ZeroOneStr ;

end;
struct ZeroOneStr -> ZeroStr , OneStr ;

aggr ZeroOneStr(# carrier, ZeroF, OneF #) -> ZeroOneStr ;

definition

let S be ZeroStr ;

func 0. S -> Element of S equals :: STRUCT_0:def 6

the ZeroF of S;

coherence

the ZeroF of S is Element of S ;

end;
func 0. S -> Element of S equals :: STRUCT_0:def 6

the ZeroF of S;

coherence

the ZeroF of S is Element of S ;

:: deftheorem defines 0. STRUCT_0:def 6 :

for S being ZeroStr holds 0. S = the ZeroF of S;

definition

let S be OneStr ;

func 1. S -> Element of S equals :: STRUCT_0:def 7

the OneF of S;

coherence

the OneF of S is Element of S ;

end;
func 1. S -> Element of S equals :: STRUCT_0:def 7

the OneF of S;

coherence

the OneF of S is Element of S ;

:: deftheorem defines 1. STRUCT_0:def 7 :

for S being OneStr holds 1. S = the OneF of S;

definition
end;

:: deftheorem Def8 defines degenerated STRUCT_0:def 8 :

for S being ZeroOneStr holds

( S is degenerated iff 0. S = 1. S );

definition

let IT be 1-sorted ;

attr IT is trivial means :Def9: :: STRUCT_0:def 9

the carrier of IT is trivial ;

end;
attr IT is trivial means :Def9: :: STRUCT_0:def 9

the carrier of IT is trivial ;

:: deftheorem Def9 defines trivial STRUCT_0:def 9 :

for IT being 1-sorted holds

( IT is trivial iff the carrier of IT is trivial );

registration

cluster empty -> trivial 1-sorted ;

coherence

for b_{1} being 1-sorted st b_{1} is empty holds

b_{1} is trivial

coherence

for b_{1} being 1-sorted st not b_{1} is trivial holds

not b_{1} is empty
;

end;
coherence

for b

b

proof end;

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

for b

not b

definition

let S be 1-sorted ;

redefine attr S is trivial means :Def10: :: STRUCT_0:def 10

for x, y being Element of S holds x = y;

compatibility

( S is trivial iff for x, y being Element of S holds x = y )

end;
redefine attr S is trivial means :Def10: :: STRUCT_0:def 10

for x, y being Element of S holds x = y;

compatibility

( S is trivial iff for x, y being Element of S holds x = y )

proof end;

:: deftheorem Def10 defines trivial STRUCT_0:def 10 :

for S being 1-sorted holds

( S is trivial iff for x, y being Element of S holds x = y );

registration

cluster non degenerated -> non trivial ZeroOneStr ;

coherence

for b_{1} being ZeroOneStr st not b_{1} is degenerated holds

not b_{1} is trivial

end;
coherence

for b

not b

proof end;

registration

cluster non empty trivial 1-sorted ;

existence

ex b_{1} being 1-sorted st

( b_{1} is trivial & not b_{1} is empty )

existence

ex b_{1} being 1-sorted st

( not b_{1} is trivial & not b_{1} is empty )

end;
existence

ex b

( b

proof end;

cluster non empty non trivial 1-sorted ;existence

ex b

( not b

proof end;

registration

let S be non trivial 1-sorted ;

cluster the carrier of S -> non trivial ;

coherence

not the carrier of S is trivial by Def9;

end;
cluster the carrier of S -> non trivial ;

coherence

not the carrier of S is trivial by Def9;

registration

let S be trivial 1-sorted ;

cluster the carrier of S -> trivial ;

coherence

the carrier of S is trivial by Def9;

end;
cluster the carrier of S -> trivial ;

coherence

the carrier of S is trivial by Def9;

begin

definition
end;

:: deftheorem Def11 defines finite STRUCT_0:def 11 :

for S being 1-sorted holds

( S is finite iff the carrier of S is finite );

registration

cluster strict non empty finite 1-sorted ;

existence

ex b_{1} being 1-sorted st

( b_{1} is strict & b_{1} is finite & not b_{1} is empty )

end;
existence

ex b

( b

proof end;

registration

let S be finite 1-sorted ;

cluster the carrier of S -> finite ;

coherence

the carrier of S is finite by Def11;

end;
cluster the carrier of S -> finite ;

coherence

the carrier of S is finite by Def11;

registration

cluster empty -> empty finite 1-sorted ;

coherence

for b_{1} being empty 1-sorted holds b_{1} is finite

end;
coherence

for b

proof end;

registration

cluster strict infinite 1-sorted ;

existence

ex b_{1} being 1-sorted st

( b_{1} is strict & not b_{1} is finite )

end;
existence

ex b

( b

proof end;

registration

let S be infinite 1-sorted ;

cluster the carrier of S -> infinite ;

coherence

not the carrier of S is finite by Def11;

end;
cluster the carrier of S -> infinite ;

coherence

not the carrier of S is finite by Def11;

registration

cluster infinite -> non empty infinite 1-sorted ;

coherence

for b_{1} being infinite 1-sorted holds not b_{1} is empty
;

end;
coherence

for b

registration

cluster trivial -> finite 1-sorted ;

coherence

for b_{1} being 1-sorted st b_{1} is trivial holds

b_{1} is finite

end;
coherence

for b

b

proof end;

registration

cluster infinite -> non trivial 1-sorted ;

coherence

for b_{1} being 1-sorted st not b_{1} is finite holds

not b_{1} is trivial
;

end;
coherence

for b

not b

definition
end;

:: deftheorem Def12 defines zero STRUCT_0:def 12 :

for S being ZeroStr

for x being Element of S holds

( x is zero iff x = 0. S );

registration

cluster strict non degenerated ZeroOneStr ;

existence

ex b_{1} being ZeroOneStr st

( b_{1} is strict & not b_{1} is degenerated )

end;
existence

ex b

( b

proof end;

registration

let S be non degenerated ZeroOneStr ;

cluster 1. S -> non zero ;

coherence

not 1. S is zero

end;
cluster 1. S -> non zero ;

coherence

not 1. S is zero

proof end;

registration
end;

begin

definition

attr c_{1} is strict ;

struct 2-sorted -> 1-sorted ;

aggr 2-sorted(# carrier, carrier' #) -> 2-sorted ;

sel carrier' c_{1} -> set ;

end;
struct 2-sorted -> 1-sorted ;

aggr 2-sorted(# carrier, carrier' #) -> 2-sorted ;

sel carrier' c

definition
end;

:: deftheorem Def13 defines void STRUCT_0:def 13 :

for S being 2-sorted holds

( S is void iff the carrier' of S is empty );

registration

cluster empty strict void 2-sorted ;

existence

ex b_{1} being 2-sorted st

( b_{1} is strict & b_{1} is empty & b_{1} is void )

end;
existence

ex b

( b

proof end;

registration

let S be void 2-sorted ;

cluster the carrier' of S -> empty ;

coherence

the carrier' of S is empty by Def13;

end;
cluster the carrier' of S -> empty ;

coherence

the carrier' of S is empty by Def13;

registration

cluster non empty strict non void 2-sorted ;

existence

ex b_{1} being 2-sorted st

( b_{1} is strict & not b_{1} is empty & not b_{1} is void )

end;
existence

ex b

( b

proof end;

registration

let S be non void 2-sorted ;

cluster the carrier' of S -> non empty ;

coherence

not the carrier' of S is empty by Def13;

end;
cluster the carrier' of S -> non empty ;

coherence

not the carrier' of S is empty by Def13;

definition

let X be 1-sorted ;

let Y be non empty 1-sorted ;

let y be Element of Y;

func X --> y -> Function of X,Y equals :: STRUCT_0:def 14

the carrier of X --> y;

coherence

the carrier of X --> y is Function of X,Y ;

end;
let Y be non empty 1-sorted ;

let y be Element of Y;

func X --> y -> Function of X,Y equals :: STRUCT_0:def 14

the carrier of X --> y;

coherence

the carrier of X --> y is Function of X,Y ;

:: deftheorem defines --> STRUCT_0:def 14 :

for X being 1-sorted

for Y being non empty 1-sorted

for y being Element of Y holds X --> y = the carrier of X --> y;

registration

let S be ZeroStr ;

cluster zero Element of the carrier of S;

existence

ex b_{1} being Element of S st b_{1} is zero

end;
cluster zero Element of the carrier of S;

existence

ex b

proof end;

registration

cluster strict non trivial ZeroStr ;

existence

ex b_{1} being ZeroStr st

( b_{1} is strict & not b_{1} is trivial )

end;
existence

ex b

( b

proof end;

registration

let S be non trivial ZeroStr ;

cluster non zero Element of the carrier of S;

existence

not for b_{1} being Element of S holds b_{1} is zero

end;
cluster non zero Element of the carrier of S;

existence

not for b

proof end;

definition

canceled;

let X be set ;

let S be ZeroStr ;

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

attr R is non-zero means :: STRUCT_0:def 16

not 0. S in rng R;

end;
let X be set ;

let S be ZeroStr ;

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

attr R is non-zero means :: STRUCT_0:def 16

not 0. S in rng R;

:: deftheorem STRUCT_0:def 15 :

canceled;

:: deftheorem defines non-zero STRUCT_0:def 16 :

for X being set

for S being ZeroStr

for R being Relation of X, the carrier of S holds

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

definition

let S be 1-sorted ;

func card S -> Cardinal equals :: STRUCT_0:def 17

card the carrier of S;

coherence

card the carrier of S is Cardinal ;

end;
func card S -> Cardinal equals :: STRUCT_0:def 17

card the carrier of S;

coherence

card the carrier of S is Cardinal ;

:: deftheorem defines card STRUCT_0:def 17 :

for S being 1-sorted holds card S = card the carrier of S;

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;
mode UnOp of S is UnOp of the carrier of S;

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

definition

let S be ZeroStr ;

func NonZero S -> Subset of S equals :: STRUCT_0:def 18

([#] S) \ {(0. S)};

coherence

([#] S) \ {(0. S)} is Subset of S ;

end;
func NonZero S -> Subset of S equals :: STRUCT_0:def 18

([#] S) \ {(0. S)};

coherence

([#] S) \ {(0. S)} is Subset of S ;

:: deftheorem defines NonZero STRUCT_0:def 18 :

for S being ZeroStr holds NonZero S = ([#] S) \ {(0. S)};

theorem :: STRUCT_0:1

proof end;

definition

let V be non empty ZeroStr ;

redefine attr V is trivial means :Def19: :: STRUCT_0:def 19

for u being Element of V holds u = 0. V;

compatibility

( V is trivial iff for u being Element of V holds u = 0. V )

end;
redefine attr V is trivial means :Def19: :: STRUCT_0:def 19

for u being Element of V holds u = 0. V;

compatibility

( V is trivial iff for u being Element of V holds u = 0. V )

proof end;

:: deftheorem Def19 defines trivial STRUCT_0:def 19 :

for V being non empty ZeroStr holds

( V is trivial iff for u being Element of V holds u = 0. V );

registration

let V be non trivial ZeroStr ;

cluster NonZero V -> non empty ;

coherence

not NonZero V is empty

end;
cluster NonZero V -> non empty ;

coherence

not NonZero V is empty

proof end;

registration

let S be non empty 1-sorted ;

cluster non empty trivial Element of K21( the carrier of S);

existence

ex b_{1} being Subset of S st

( not b_{1} is empty & b_{1} is trivial )

end;
cluster non empty trivial Element of K21( the carrier of S);

existence

ex b

( not b

proof end;

theorem :: STRUCT_0:2

proof end;