:: by Andrzej Trybulec

::

:: Received September 18, 1989

:: Copyright (c) 1990-2012 Association of Mizar Users

begin

theorem Th7: :: SETWISEO:7

for Y, X being non empty set

for f being Function of X,Y

for x being Element of X holds x in f " {(f . x)}

for f being Function of X,Y

for x being Element of X holds x in f " {(f . x)}

proof end;

theorem Th8: :: SETWISEO:8

for Y, X being non empty set

for f being Function of X,Y

for x being Element of X holds Im (f,x) = {(f . x)}

for f being Function of X,Y

for x being Element of X holds Im (f,x) = {(f . x)}

proof end;

:: Theorems related to Fin ...

theorem Th9: :: SETWISEO:9

for X being non empty set

for B being Element of Fin X

for x being set st x in B holds

x is Element of X

for B being Element of Fin X

for x being set st x in B holds

x is Element of X

proof end;

theorem :: SETWISEO:10

for X, Y being non empty set

for A being Element of Fin X

for B being set

for f being Function of X,Y st ( for x being Element of X st x in A holds

f . x in B ) holds

f .: A c= B

for A being Element of Fin X

for B being set

for f being Function of X,Y st ( for x being Element of X st x in A holds

f . x in B ) holds

f .: A c= B

proof end;

Lm1: for X, Y being non empty set

for f being Function of X,Y

for A being Element of Fin X holds f .: A is Element of Fin Y

by FINSUB_1:def 5;

theorem Th12: :: SETWISEO:12

for X being non empty set

for B being Element of Fin X st B <> {} holds

ex x being Element of X st x in B

for B being Element of Fin X st B <> {} holds

ex x being Element of X st x in B

proof end;

theorem Th13: :: SETWISEO:13

for Y, X being non empty set

for f being Function of X,Y

for A being Element of Fin X st f .: A = {} holds

A = {}

for f being Function of X,Y

for A being Element of Fin X st f .: A = {} holds

A = {}

proof end;

registration
end;

:: theorems related to BinOp of ...

definition

let X be non empty set ;

let F be BinOp of X;

end;
let F be BinOp of X;

attr F is having_a_unity means :Def2: :: SETWISEO:def 2

ex x being Element of X st x is_a_unity_wrt F;

ex x being Element of X st x is_a_unity_wrt F;

:: deftheorem Def2 defines having_a_unity SETWISEO:def 2 :

for X being non empty set

for F being BinOp of X holds

( F is having_a_unity iff ex x being Element of X st x is_a_unity_wrt F );

for X being non empty set

for F being BinOp of X holds

( F is having_a_unity iff ex x being Element of X st x is_a_unity_wrt F );

theorem Th14: :: SETWISEO:14

for X being non empty set

for F being BinOp of X holds

( F is having_a_unity iff the_unity_wrt F is_a_unity_wrt F )

for F being BinOp of X holds

( F is having_a_unity iff the_unity_wrt F is_a_unity_wrt F )

proof end;

theorem Th15: :: SETWISEO:15

for X being non empty set

for F being BinOp of X st F is having_a_unity holds

for x being Element of X holds

( F . ((the_unity_wrt F),x) = x & F . (x,(the_unity_wrt F)) = x )

for F being BinOp of X st F is having_a_unity holds

for x being Element of X holds

( F . ((the_unity_wrt F),x) = x & F . (x,(the_unity_wrt F)) = x )

proof end;

:: Main part

registration

let X be non empty set ;

existence

not for b_{1} being Element of Fin X holds b_{1} is empty

end;
existence

not for b

proof end;

notation

let X be non empty set ;

let x be Element of X;

synonym {.x.} for {X};

let y be Element of X;

synonym {.x,y.} for {X,x};

let z be Element of X;

synonym {.x,y,z.} for {X,x,y};

end;
let x be Element of X;

synonym {.x.} for {X};

let y be Element of X;

synonym {.x,y.} for {X,x};

let z be Element of X;

synonym {.x,y,z.} for {X,x,y};

definition

let X be non empty set ;

let x be Element of X;

:: original: {.

redefine func {.x.} -> Element of Fin X;

coherence

{..} is Element of Fin X

:: original: {.

redefine func {.x,y.} -> Element of Fin X;

coherence

{.y,.} is Element of Fin X

:: original: {.

redefine func {.x,y,z.} -> Element of Fin X;

coherence

{.y,z,.} is Element of Fin X

end;
let x be Element of X;

:: original: {.

redefine func {.x.} -> Element of Fin X;

coherence

{..} is Element of Fin X

proof end;

let y be Element of X;:: original: {.

redefine func {.x,y.} -> Element of Fin X;

coherence

{.y,.} is Element of Fin X

proof end;

let z be Element of X;:: original: {.

redefine func {.x,y,z.} -> Element of Fin X;

coherence

{.y,z,.} is Element of Fin X

proof end;

definition

let X be set ;

let A, B be Element of Fin X;

:: original: \/

redefine func A \/ B -> Element of Fin X;

coherence

A \/ B is Element of Fin X by FINSUB_1:1;

end;
let A, B be Element of Fin X;

:: original: \/

redefine func A \/ B -> Element of Fin X;

coherence

A \/ B is Element of Fin X by FINSUB_1:1;

definition

let X be set ;

let A, B be Element of Fin X;

:: original: \

redefine func A \ B -> Element of Fin X;

coherence

A \ B is Element of Fin X by FINSUB_1:1;

end;
let A, B be Element of Fin X;

:: original: \

redefine func A \ B -> Element of Fin X;

coherence

A \ B is Element of Fin X by FINSUB_1:1;

definition

let X, Y be non empty set ;

let F be BinOp of Y;

let B be Element of Fin X;

let f be Function of X,Y;

assume that

A1: ( B <> {} or F is having_a_unity ) and

A2: F is commutative and

A3: F is associative ;

ex b_{1} being Element of Y ex G being Function of (Fin X),Y st

( b_{1} = G . B & ( for e being Element of Y st e is_a_unity_wrt F holds

G . {} = e ) & ( for x being Element of X holds G . {x} = f . x ) & ( for B9 being Element of Fin X st B9 c= B & B9 <> {} holds

for x being Element of X st x in B \ B9 holds

G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) )

for b_{1}, b_{2} being Element of Y st ex G being Function of (Fin X),Y st

( b_{1} = G . B & ( for e being Element of Y st e is_a_unity_wrt F holds

G . {} = e ) & ( for x being Element of X holds G . {x} = f . x ) & ( for B9 being Element of Fin X st B9 c= B & B9 <> {} holds

for x being Element of X st x in B \ B9 holds

G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) & ex G being Function of (Fin X),Y st

( b_{2} = G . B & ( for e being Element of Y st e is_a_unity_wrt F holds

G . {} = e ) & ( for x being Element of X holds G . {x} = f . x ) & ( for B9 being Element of Fin X st B9 c= B & B9 <> {} holds

for x being Element of X st x in B \ B9 holds

G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) holds

b_{1} = b_{2}

end;
let F be BinOp of Y;

let B be Element of Fin X;

let f be Function of X,Y;

assume that

A1: ( B <> {} or F is having_a_unity ) and

A2: F is commutative and

A3: F is associative ;

func F $$ (B,f) -> Element of Y means :Def3: :: SETWISEO:def 3

ex G being Function of (Fin X),Y st

( it = G . B & ( for e being Element of Y st e is_a_unity_wrt F holds

G . {} = e ) & ( for x being Element of X holds G . {x} = f . x ) & ( for B9 being Element of Fin X st B9 c= B & B9 <> {} holds

for x being Element of X st x in B \ B9 holds

G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) );

existence ex G being Function of (Fin X),Y st

( it = G . B & ( for e being Element of Y st e is_a_unity_wrt F holds

G . {} = e ) & ( for x being Element of X holds G . {x} = f . x ) & ( for B9 being Element of Fin X st B9 c= B & B9 <> {} holds

for x being Element of X st x in B \ B9 holds

G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) );

ex b

( b

G . {} = e ) & ( for x being Element of X holds G . {x} = f . x ) & ( for B9 being Element of Fin X st B9 c= B & B9 <> {} holds

for x being Element of X st x in B \ B9 holds

G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) )

proof end;

uniqueness for b

( b

G . {} = e ) & ( for x being Element of X holds G . {x} = f . x ) & ( for B9 being Element of Fin X st B9 c= B & B9 <> {} holds

for x being Element of X st x in B \ B9 holds

G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) & ex G being Function of (Fin X),Y st

( b

G . {} = e ) & ( for x being Element of X holds G . {x} = f . x ) & ( for B9 being Element of Fin X st B9 c= B & B9 <> {} holds

for x being Element of X st x in B \ B9 holds

G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) holds

b

proof end;

:: deftheorem Def3 defines $$ SETWISEO:def 3 :

for X, Y being non empty set

for F being BinOp of Y

for B being Element of Fin X

for f being Function of X,Y st ( B <> {} or F is having_a_unity ) & F is commutative & F is associative holds

for b_{6} being Element of Y holds

( b_{6} = F $$ (B,f) iff ex G being Function of (Fin X),Y st

( b_{6} = G . B & ( for e being Element of Y st e is_a_unity_wrt F holds

G . {} = e ) & ( for x being Element of X holds G . {x} = f . x ) & ( for B9 being Element of Fin X st B9 c= B & B9 <> {} holds

for x being Element of X st x in B \ B9 holds

G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) );

for X, Y being non empty set

for F being BinOp of Y

for B being Element of Fin X

for f being Function of X,Y st ( B <> {} or F is having_a_unity ) & F is commutative & F is associative holds

for b

( b

( b

G . {} = e ) & ( for x being Element of X holds G . {x} = f . x ) & ( for B9 being Element of Fin X st B9 c= B & B9 <> {} holds

for x being Element of X st x in B \ B9 holds

G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) );

theorem Th16: :: SETWISEO:16

for X, Y being non empty set

for F being BinOp of Y

for B being Element of Fin X

for f being Function of X,Y st ( B <> {} or F is having_a_unity ) & F is idempotent & F is commutative & F is associative holds

for IT being Element of Y holds

( IT = F $$ (B,f) iff ex G being Function of (Fin X),Y st

( IT = G . B & ( for e being Element of Y st e is_a_unity_wrt F holds

G . {} = e ) & ( for x being Element of X holds G . {x} = f . x ) & ( for B9 being Element of Fin X st B9 c= B & B9 <> {} holds

for x being Element of X st x in B holds

G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) )

for F being BinOp of Y

for B being Element of Fin X

for f being Function of X,Y st ( B <> {} or F is having_a_unity ) & F is idempotent & F is commutative & F is associative holds

for IT being Element of Y holds

( IT = F $$ (B,f) iff ex G being Function of (Fin X),Y st

( IT = G . B & ( for e being Element of Y st e is_a_unity_wrt F holds

G . {} = e ) & ( for x being Element of X holds G . {x} = f . x ) & ( for B9 being Element of Fin X st B9 c= B & B9 <> {} holds

for x being Element of X st x in B holds

G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) )

proof end;

theorem Th17: :: SETWISEO:17

for Y, X being non empty set

for F being BinOp of Y

for f being Function of X,Y st F is commutative & F is associative holds

for b being Element of X holds F $$ ({.b.},f) = f . b

for F being BinOp of Y

for f being Function of X,Y st F is commutative & F is associative holds

for b being Element of X holds F $$ ({.b.},f) = f . b

proof end;

theorem Th18: :: SETWISEO:18

for Y, X being non empty set

for F being BinOp of Y

for f being Function of X,Y st F is idempotent & F is commutative & F is associative holds

for a, b being Element of X holds F $$ ({.a,b.},f) = F . ((f . a),(f . b))

for F being BinOp of Y

for f being Function of X,Y st F is idempotent & F is commutative & F is associative holds

for a, b being Element of X holds F $$ ({.a,b.},f) = F . ((f . a),(f . b))

proof end;

theorem Th19: :: SETWISEO:19

for Y, X being non empty set

for F being BinOp of Y

for f being Function of X,Y st F is idempotent & F is commutative & F is associative holds

for a, b, c being Element of X holds F $$ ({.a,b,c.},f) = F . ((F . ((f . a),(f . b))),(f . c))

for F being BinOp of Y

for f being Function of X,Y st F is idempotent & F is commutative & F is associative holds

for a, b, c being Element of X holds F $$ ({.a,b,c.},f) = F . ((F . ((f . a),(f . b))),(f . c))

proof end;

:: If B is non empty

theorem Th20: :: SETWISEO:20

for Y, X being non empty set

for F being BinOp of Y

for B being Element of Fin X

for f being Function of X,Y st F is idempotent & F is commutative & F is associative & B <> {} holds

for x being Element of X holds F $$ ((B \/ {.x.}),f) = F . ((F $$ (B,f)),(f . x))

for F being BinOp of Y

for B being Element of Fin X

for f being Function of X,Y st F is idempotent & F is commutative & F is associative & B <> {} holds

for x being Element of X holds F $$ ((B \/ {.x.}),f) = F . ((F $$ (B,f)),(f . x))

proof end;

theorem Th21: :: SETWISEO:21

for Y, X being non empty set

for F being BinOp of Y

for f being Function of X,Y st F is idempotent & F is commutative & F is associative holds

for B1, B2 being Element of Fin X st B1 <> {} & B2 <> {} holds

F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f)))

for F being BinOp of Y

for f being Function of X,Y st F is idempotent & F is commutative & F is associative holds

for B1, B2 being Element of Fin X st B1 <> {} & B2 <> {} holds

F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f)))

proof end;

theorem :: SETWISEO:22

for Y, X being non empty set

for F being BinOp of Y

for B being Element of Fin X

for f being Function of X,Y st F is commutative & F is associative & F is idempotent holds

for x being Element of X st x in B holds

F . ((f . x),(F $$ (B,f))) = F $$ (B,f)

for F being BinOp of Y

for B being Element of Fin X

for f being Function of X,Y st F is commutative & F is associative & F is idempotent holds

for x being Element of X st x in B holds

F . ((f . x),(F $$ (B,f))) = F $$ (B,f)

proof end;

theorem :: SETWISEO:23

for Y, X being non empty set

for F being BinOp of Y

for f being Function of X,Y st F is commutative & F is associative & F is idempotent holds

for B, C being Element of Fin X st B <> {} & B c= C holds

F . ((F $$ (B,f)),(F $$ (C,f))) = F $$ (C,f)

for F being BinOp of Y

for f being Function of X,Y st F is commutative & F is associative & F is idempotent holds

for B, C being Element of Fin X st B <> {} & B c= C holds

F . ((F $$ (B,f)),(F $$ (C,f))) = F $$ (C,f)

proof end;

theorem Th24: :: SETWISEO:24

for Y, X being non empty set

for F being BinOp of Y

for B being Element of Fin X

for f being Function of X,Y st B <> {} & F is commutative & F is associative & F is idempotent holds

for a being Element of Y st ( for b being Element of X st b in B holds

f . b = a ) holds

F $$ (B,f) = a

for F being BinOp of Y

for B being Element of Fin X

for f being Function of X,Y st B <> {} & F is commutative & F is associative & F is idempotent holds

for a being Element of Y st ( for b being Element of X st b in B holds

f . b = a ) holds

F $$ (B,f) = a

proof end;

theorem Th25: :: SETWISEO:25

for X, Y being non empty set

for F being BinOp of Y

for B being Element of Fin X

for f being Function of X,Y st F is commutative & F is associative & F is idempotent holds

for a being Element of Y st f .: B = {a} holds

F $$ (B,f) = a

for F being BinOp of Y

for B being Element of Fin X

for f being Function of X,Y st F is commutative & F is associative & F is idempotent holds

for a being Element of Y st f .: B = {a} holds

F $$ (B,f) = a

proof end;

theorem Th26: :: SETWISEO:26

for X, Y being non empty set

for F being BinOp of Y st F is commutative & F is associative & F is idempotent holds

for f, g being Function of X,Y

for A, B being Element of Fin X st A <> {} & f .: A = g .: B holds

F $$ (A,f) = F $$ (B,g)

for F being BinOp of Y st F is commutative & F is associative & F is idempotent holds

for f, g being Function of X,Y

for A, B being Element of Fin X st A <> {} & f .: A = g .: B holds

F $$ (A,f) = F $$ (B,g)

proof end;

theorem :: SETWISEO:27

for Y, X being non empty set

for F, G being BinOp of Y st F is idempotent & F is commutative & F is associative & G is_distributive_wrt F holds

for B being Element of Fin X st B <> {} holds

for f being Function of X,Y

for a being Element of Y holds G . (a,(F $$ (B,f))) = F $$ (B,(G [;] (a,f)))

for F, G being BinOp of Y st F is idempotent & F is commutative & F is associative & G is_distributive_wrt F holds

for B being Element of Fin X st B <> {} holds

for f being Function of X,Y

for a being Element of Y holds G . (a,(F $$ (B,f))) = F $$ (B,(G [;] (a,f)))

proof end;

theorem :: SETWISEO:28

for Y, X being non empty set

for F, G being BinOp of Y st F is idempotent & F is commutative & F is associative & G is_distributive_wrt F holds

for B being Element of Fin X st B <> {} holds

for f being Function of X,Y

for a being Element of Y holds G . ((F $$ (B,f)),a) = F $$ (B,(G [:] (f,a)))

for F, G being BinOp of Y st F is idempotent & F is commutative & F is associative & G is_distributive_wrt F holds

for B being Element of Fin X st B <> {} holds

for f being Function of X,Y

for a being Element of Y holds G . ((F $$ (B,f)),a) = F $$ (B,(G [:] (f,a)))

proof end;

definition

let X, Y be non empty set ;

let f be Function of X,Y;

let A be Element of Fin X;

:: original: .:

redefine func f .: A -> Element of Fin Y;

coherence

f .: A is Element of Fin Y by Lm1;

end;
let f be Function of X,Y;

let A be Element of Fin X;

:: original: .:

redefine func f .: A -> Element of Fin Y;

coherence

f .: A is Element of Fin Y by Lm1;

theorem Th29: :: SETWISEO:29

for A, X, Y being non empty set

for F being BinOp of A st F is idempotent & F is commutative & F is associative holds

for B being Element of Fin X st B <> {} holds

for f being Function of X,Y

for g being Function of Y,A holds F $$ ((f .: B),g) = F $$ (B,(g * f))

for F being BinOp of A st F is idempotent & F is commutative & F is associative holds

for B being Element of Fin X st B <> {} holds

for f being Function of X,Y

for g being Function of Y,A holds F $$ ((f .: B),g) = F $$ (B,(g * f))

proof end;

theorem Th30: :: SETWISEO:30

for X, Y being non empty set

for F being BinOp of Y st F is commutative & F is associative & F is idempotent holds

for Z being non empty set

for G being BinOp of Z st G is commutative & G is associative & G is idempotent holds

for f being Function of X,Y

for g being Function of Y,Z st ( for x, y being Element of Y holds g . (F . (x,y)) = G . ((g . x),(g . y)) ) holds

for B being Element of Fin X st B <> {} holds

g . (F $$ (B,f)) = G $$ (B,(g * f))

for F being BinOp of Y st F is commutative & F is associative & F is idempotent holds

for Z being non empty set

for G being BinOp of Z st G is commutative & G is associative & G is idempotent holds

for f being Function of X,Y

for g being Function of Y,Z st ( for x, y being Element of Y holds g . (F . (x,y)) = G . ((g . x),(g . y)) ) holds

for B being Element of Fin X st B <> {} holds

g . (F $$ (B,f)) = G $$ (B,(g * f))

proof end;

:: If F has a unity

theorem Th31: :: SETWISEO:31

for Y, X being non empty set

for F being BinOp of Y st F is commutative & F is associative & F is having_a_unity holds

for f being Function of X,Y holds F $$ (({}. X),f) = the_unity_wrt F

for F being BinOp of Y st F is commutative & F is associative & F is having_a_unity holds

for f being Function of X,Y holds F $$ (({}. X),f) = the_unity_wrt F

proof end;

theorem Th32: :: SETWISEO:32

for Y, X being non empty set

for F being BinOp of Y

for B being Element of Fin X

for f being Function of X,Y st F is idempotent & F is commutative & F is associative & F is having_a_unity holds

for x being Element of X holds F $$ ((B \/ {.x.}),f) = F . ((F $$ (B,f)),(f . x))

for F being BinOp of Y

for B being Element of Fin X

for f being Function of X,Y st F is idempotent & F is commutative & F is associative & F is having_a_unity holds

for x being Element of X holds F $$ ((B \/ {.x.}),f) = F . ((F $$ (B,f)),(f . x))

proof end;

theorem :: SETWISEO:33

for Y, X being non empty set

for F being BinOp of Y

for f being Function of X,Y st F is idempotent & F is commutative & F is associative & F is having_a_unity holds

for B1, B2 being Element of Fin X holds F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f)))

for F being BinOp of Y

for f being Function of X,Y st F is idempotent & F is commutative & F is associative & F is having_a_unity holds

for B1, B2 being Element of Fin X holds F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f)))

proof end;

theorem :: SETWISEO:34

for X, Y being non empty set

for F being BinOp of Y st F is commutative & F is associative & F is idempotent & F is having_a_unity holds

for f, g being Function of X,Y

for A, B being Element of Fin X st f .: A = g .: B holds

F $$ (A,f) = F $$ (B,g)

for F being BinOp of Y st F is commutative & F is associative & F is idempotent & F is having_a_unity holds

for f, g being Function of X,Y

for A, B being Element of Fin X st f .: A = g .: B holds

F $$ (A,f) = F $$ (B,g)

proof end;

theorem Th35: :: SETWISEO:35

for A, X, Y being non empty set

for F being BinOp of A st F is idempotent & F is commutative & F is associative & F is having_a_unity holds

for B being Element of Fin X

for f being Function of X,Y

for g being Function of Y,A holds F $$ ((f .: B),g) = F $$ (B,(g * f))

for F being BinOp of A st F is idempotent & F is commutative & F is associative & F is having_a_unity holds

for B being Element of Fin X

for f being Function of X,Y

for g being Function of Y,A holds F $$ ((f .: B),g) = F $$ (B,(g * f))

proof end;

theorem :: SETWISEO:36

for X, Y being non empty set

for F being BinOp of Y st F is commutative & F is associative & F is idempotent & F is having_a_unity holds

for Z being non empty set

for G being BinOp of Z st G is commutative & G is associative & G is idempotent & G is having_a_unity holds

for f being Function of X,Y

for g being Function of Y,Z st g . (the_unity_wrt F) = the_unity_wrt G & ( for x, y being Element of Y holds g . (F . (x,y)) = G . ((g . x),(g . y)) ) holds

for B being Element of Fin X holds g . (F $$ (B,f)) = G $$ (B,(g * f))

for F being BinOp of Y st F is commutative & F is associative & F is idempotent & F is having_a_unity holds

for Z being non empty set

for G being BinOp of Z st G is commutative & G is associative & G is idempotent & G is having_a_unity holds

for f being Function of X,Y

for g being Function of Y,Z st g . (the_unity_wrt F) = the_unity_wrt G & ( for x, y being Element of Y holds g . (F . (x,y)) = G . ((g . x),(g . y)) ) holds

for B being Element of Fin X holds g . (F $$ (B,f)) = G $$ (B,(g * f))

proof end;

definition

let A be set ;

ex b_{1} being BinOp of (Fin A) st

for x, y being Element of Fin A holds b_{1} . (x,y) = x \/ y

for b_{1}, b_{2} being BinOp of (Fin A) st ( for x, y being Element of Fin A holds b_{1} . (x,y) = x \/ y ) & ( for x, y being Element of Fin A holds b_{2} . (x,y) = x \/ y ) holds

b_{1} = b_{2}

end;
func FinUnion A -> BinOp of (Fin A) means :Def4: :: SETWISEO:def 4

for x, y being Element of Fin A holds it . (x,y) = x \/ y;

existence for x, y being Element of Fin A holds it . (x,y) = x \/ y;

ex b

for x, y being Element of Fin A holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines FinUnion SETWISEO:def 4 :

for A being set

for b_{2} being BinOp of (Fin A) holds

( b_{2} = FinUnion A iff for x, y being Element of Fin A holds b_{2} . (x,y) = x \/ y );

for A being set

for b

( b

definition

let X be non empty set ;

let A be set ;

let B be Element of Fin X;

let f be Function of X,(Fin A);

coherence

(FinUnion A) $$ (B,f) is Element of Fin A ;

end;
let A be set ;

let B be Element of Fin X;

let f be Function of X,(Fin A);

coherence

(FinUnion A) $$ (B,f) is Element of Fin A ;

:: deftheorem defines FinUnion SETWISEO:def 5 :

for X being non empty set

for A being set

for B being Element of Fin X

for f being Function of X,(Fin A) holds FinUnion (B,f) = (FinUnion A) $$ (B,f);

for X being non empty set

for A being set

for B being Element of Fin X

for f being Function of X,(Fin A) holds FinUnion (B,f) = (FinUnion A) $$ (B,f);

theorem :: SETWISEO:44

for X being non empty set

for A being set

for f being Function of X,(Fin A)

for i being Element of X holds FinUnion ({.i.},f) = f . i

for A being set

for f being Function of X,(Fin A)

for i being Element of X holds FinUnion ({.i.},f) = f . i

proof end;

theorem :: SETWISEO:45

for X being non empty set

for A being set

for f being Function of X,(Fin A)

for i, j being Element of X holds FinUnion ({.i,j.},f) = (f . i) \/ (f . j)

for A being set

for f being Function of X,(Fin A)

for i, j being Element of X holds FinUnion ({.i,j.},f) = (f . i) \/ (f . j)

proof end;

theorem :: SETWISEO:46

for X being non empty set

for A being set

for f being Function of X,(Fin A)

for i, j, k being Element of X holds FinUnion ({.i,j,k.},f) = ((f . i) \/ (f . j)) \/ (f . k)

for A being set

for f being Function of X,(Fin A)

for i, j, k being Element of X holds FinUnion ({.i,j,k.},f) = ((f . i) \/ (f . j)) \/ (f . k)

proof end;

theorem Th47: :: SETWISEO:47

for X being non empty set

for A being set

for f being Function of X,(Fin A) holds FinUnion (({}. X),f) = {}

for A being set

for f being Function of X,(Fin A) holds FinUnion (({}. X),f) = {}

proof end;

theorem Th48: :: SETWISEO:48

for X being non empty set

for A being set

for f being Function of X,(Fin A)

for i being Element of X

for B being Element of Fin X holds FinUnion ((B \/ {.i.}),f) = (FinUnion (B,f)) \/ (f . i)

for A being set

for f being Function of X,(Fin A)

for i being Element of X

for B being Element of Fin X holds FinUnion ((B \/ {.i.}),f) = (FinUnion (B,f)) \/ (f . i)

proof end;

theorem Th49: :: SETWISEO:49

for X being non empty set

for A being set

for f being Function of X,(Fin A)

for B being Element of Fin X holds FinUnion (B,f) = union (f .: B)

for A being set

for f being Function of X,(Fin A)

for B being Element of Fin X holds FinUnion (B,f) = union (f .: B)

proof end;

theorem :: SETWISEO:50

for X being non empty set

for A being set

for f being Function of X,(Fin A)

for B1, B2 being Element of Fin X holds FinUnion ((B1 \/ B2),f) = (FinUnion (B1,f)) \/ (FinUnion (B2,f))

for A being set

for f being Function of X,(Fin A)

for B1, B2 being Element of Fin X holds FinUnion ((B1 \/ B2),f) = (FinUnion (B1,f)) \/ (FinUnion (B2,f))

proof end;

theorem :: SETWISEO:51

for X, Y being non empty set

for A being set

for B being Element of Fin X

for f being Function of X,Y

for g being Function of Y,(Fin A) holds FinUnion ((f .: B),g) = FinUnion (B,(g * f))

for A being set

for B being Element of Fin X

for f being Function of X,Y

for g being Function of Y,(Fin A) holds FinUnion ((f .: B),g) = FinUnion (B,(g * f))

proof end;

theorem Th52: :: SETWISEO:52

for A, X being non empty set

for Y being set

for G being BinOp of A st G is commutative & G is associative & G is idempotent holds

for B being Element of Fin X st B <> {} holds

for f being Function of X,(Fin Y)

for g being Function of (Fin Y),A st ( for x, y being Element of Fin Y holds g . (x \/ y) = G . ((g . x),(g . y)) ) holds

g . (FinUnion (B,f)) = G $$ (B,(g * f))

for Y being set

for G being BinOp of A st G is commutative & G is associative & G is idempotent holds

for B being Element of Fin X st B <> {} holds

for f being Function of X,(Fin Y)

for g being Function of (Fin Y),A st ( for x, y being Element of Fin Y holds g . (x \/ y) = G . ((g . x),(g . y)) ) holds

g . (FinUnion (B,f)) = G $$ (B,(g * f))

proof end;

theorem Th53: :: SETWISEO:53

for X, Z being non empty set

for Y being set

for G being BinOp of Z st G is commutative & G is associative & G is idempotent & G is having_a_unity holds

for f being Function of X,(Fin Y)

for g being Function of (Fin Y),Z st g . ({}. Y) = the_unity_wrt G & ( for x, y being Element of Fin Y holds g . (x \/ y) = G . ((g . x),(g . y)) ) holds

for B being Element of Fin X holds g . (FinUnion (B,f)) = G $$ (B,(g * f))

for Y being set

for G being BinOp of Z st G is commutative & G is associative & G is idempotent & G is having_a_unity holds

for f being Function of X,(Fin Y)

for g being Function of (Fin Y),Z st g . ({}. Y) = the_unity_wrt G & ( for x, y being Element of Fin Y holds g . (x \/ y) = G . ((g . x),(g . y)) ) holds

for B being Element of Fin X holds g . (FinUnion (B,f)) = G $$ (B,(g * f))

proof end;

definition

let A be set ;

ex b_{1} being Function of A,(Fin A) st

for x being set st x in A holds

b_{1} . x = {x}

for b_{1}, b_{2} being Function of A,(Fin A) st ( for x being set st x in A holds

b_{1} . x = {x} ) & ( for x being set st x in A holds

b_{2} . x = {x} ) holds

b_{1} = b_{2}

end;
func singleton A -> Function of A,(Fin A) means :Def6: :: SETWISEO:def 6

for x being set st x in A holds

it . x = {x};

existence for x being set st x in A holds

it . x = {x};

ex b

for x being set st x in A holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def6 defines singleton SETWISEO:def 6 :

for A being set

for b_{2} being Function of A,(Fin A) holds

( b_{2} = singleton A iff for x being set st x in A holds

b_{2} . x = {x} );

for A being set

for b

( b

b

theorem Th54: :: SETWISEO:54

for A being non empty set

for f being Function of A,(Fin A) holds

( f = singleton A iff for x being Element of A holds f . x = {x} )

for f being Function of A,(Fin A) holds

( f = singleton A iff for x being Element of A holds f . x = {x} )

proof end;

theorem Th55: :: SETWISEO:55

for X being non empty set

for x being set

for y being Element of X holds

( x in (singleton X) . y iff x = y )

for x being set

for y being Element of X holds

( x in (singleton X) . y iff x = y )

proof end;

theorem :: SETWISEO:56

for X being non empty set

for x, y, z being Element of X st x in (singleton X) . z & y in (singleton X) . z holds

x = y

for x, y, z being Element of X st x in (singleton X) . z & y in (singleton X) . z holds

x = y

proof end;

Lm2: for D being non empty set

for X, P being set

for f being Function of X,D holds f .: P c= D

;

theorem Th57: :: SETWISEO:57

for X being non empty set

for A being set

for f being Function of X,(Fin A)

for B being Element of Fin X

for x being set holds

( x in FinUnion (B,f) iff ex i being Element of X st

( i in B & x in f . i ) )

for A being set

for f being Function of X,(Fin A)

for B being Element of Fin X

for x being set holds

( x in FinUnion (B,f) iff ex i being Element of X st

( i in B & x in f . i ) )

proof end;

theorem :: SETWISEO:59

for X being non empty set

for Y, Z being set

for f being Function of X,(Fin Y)

for g being Function of (Fin Y),(Fin Z) st g . ({}. Y) = {}. Z & ( for x, y being Element of Fin Y holds g . (x \/ y) = (g . x) \/ (g . y) ) holds

for B being Element of Fin X holds g . (FinUnion (B,f)) = FinUnion (B,(g * f))

for Y, Z being set

for f being Function of X,(Fin Y)

for g being Function of (Fin Y),(Fin Z) st g . ({}. Y) = {}. Z & ( for x, y being Element of Fin Y holds g . (x \/ y) = (g . x) \/ (g . y) ) holds

for B being Element of Fin X holds g . (FinUnion (B,f)) = FinUnion (B,(g * f))

proof end;