:: SETWISEO semantic presentation

theorem Th1: :: SETWISEO:1

canceled;

theorem Th2: :: SETWISEO:2

canceled;

theorem Th3: :: SETWISEO:3

for b₁, b₂, b₃ being set holds {b₁} c= {b₁,b₂,b₃}

proof end;

theorem Th4: :: SETWISEO:4

for b₁, b₂, b₃ being set holds {b₁,b₂} c= {b₁,b₂,b₃}

proof end;

theorem Th5: :: SETWISEO:5

for b₁, b₂, b₃ being set holds
( not b₁ c= b₂ \/ {b₃} or b₃ in b₁ or b₁ c= b₂ )

proof end;

theorem Th6: :: SETWISEO:6

for b₁, b₂, b₃ being set holds
( b₁ in b₂ \/ {b₃} iff ( b₁ in b₂ or b₁ = b₃ ) )

proof end;

theorem Th7: :: SETWISEO:7

canceled;

theorem Th8: :: SETWISEO:8

for b₁, b₂, b₃ being set holds
( b₁ \/ {b₂} c= b₃ iff ( b₂ in b₃ & b₁ c= b₃ ) )

proof end;

theorem Th9: :: SETWISEO:9

canceled;

theorem Th10: :: SETWISEO:10

canceled;

theorem Th11: :: SETWISEO:11

for b₁, b₂ being set
for b₃ being Function holds b₃ .: (b₂ \ (b₃ " b₁)) = (b₃ .: b₂) \ b₁

proof end;

theorem Th12: :: SETWISEO:12

for b₁, b₂ being non empty set
for b₃ being Function of b₂,b₁
for b₄ being Element of b₂ holds b₄ in b₃ " {(b₃ . b₄)}

proof end;

theorem Th13: :: SETWISEO:13

for b₁, b₂ being non empty set
for b₃ being Function of b₂,b₁
for b₄ being Element of b₂ holds b₃ .: {b₄} = {(b₃ . b₄)}

proof end;

theorem Th14: :: SETWISEO:14

for b₁ being non empty set
for b₂ being Element of Fin b₁
for b₃ being set st b₃ in b₂ holds
b₃ is Element of b₁

proof end;

theorem Th15: :: SETWISEO:15

for b₁, b₂ being non empty set
for b₃ being Element of Fin b₁
for b₄ being set
for b₅ being Function of b₁,b₂ st ( for b₆ being Element of b₁ st b₆ in b₃ holds
b₅ . b₆ in b₄ ) holds
b₅ .: b₃ c= b₄

proof end;

theorem Th16: :: SETWISEO:16

for b₁ being set
for b₂ being Element of Fin b₁
for b₃ being set st b₃ c= b₂ holds
b₃ is Element of Fin b₁

proof end;

Lemma11: for b₁, b₂ being non empty set
for b₃ being Function of b₁,b₂
for b₄ being Element of Fin b₁ holds b₃ .: b₄ is Element of Fin b₂
by FINSUB_1:def 5;

theorem Th17: :: SETWISEO:17

canceled;

theorem Th18: :: SETWISEO:18

for b₁ being non empty set
for b₂ being Element of Fin b₁ st b₂ <> {} holds
ex b₃ being Element of b₁ st b₃ in b₂

proof end;

theorem Th19: :: SETWISEO:19

for b₁, b₂ being non empty set
for b₃ being Function of b₂,b₁
for b₄ being Element of Fin b₂ st b₃ .: b₄ = {} holds
b₄ = {}

proof end;

registration

let c₁ be set ;
cluster empty Element of Fin a₁;
existence

proof end;

end;

definition

let c₁ be set ;
func {}. c₁ -> empty Element of Fin a₁ equals :: SETWISEO:def 1
{} ;
coherence by FINSUB_1:18;

end;

:: deftheorem Def1 defines {}. SETWISEO:def 1 :

scheme :: SETWISEO:sch 1
s1{ F₁() -> non empty set , F₂() -> Element of Fin F₁(), P₁[ set , set ] } :

ex b₁ being Function of F₁(), Fin F₁() st
for b₂, b₃ being Element of F₁() holds
( b₃ in b₁ . b₂ iff ( b₃ in F₂() & P₁[b₃,b₂] ) )

proof end;

definition

let c₁ be non empty set ;
let c₂ be BinOp of c₁;
attr a₂ is having_a_unity means :Def2: :: SETWISEO:def 2
ex b₁ being Element of a₁ st b₁ is_a_unity_wrt a₂;

end;

:: deftheorem Def2 defines having_a_unity SETWISEO:def 2 :

notation

let c₁ be non empty set ;
let c₂ be BinOp of c₁;
synonym c₂ has_a_unity for having_a_unity c₂;

end;

theorem Th20: :: SETWISEO:20

canceled;

theorem Th21: :: SETWISEO:21

canceled;

theorem Th22: :: SETWISEO:22

for b₁ being non empty set
for b₂ being BinOp of b₁ holds
( b₂ has_a_unity iff the_unity_wrt b₂ is_a_unity_wrt b₂ )

proof end;

theorem Th23: :: SETWISEO:23

for b₁ being non empty set
for b₂ being BinOp of b₁ st b₂ has_a_unity holds
for b₃ being Element of b₁ holds
( b₂ . (the_unity_wrt b₂),b₃ = b₃ & b₂ . b₃,(the_unity_wrt b₂) = b₃ )

proof end;

registration

let c₁ be non empty set ;
cluster non empty Element of Fin a₁;
existence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be Element of c₁;
redefine func { as {c₂} -> Element of Fin a₁;
coherence

proof end;

let c₃ be Element of c₁;
redefine func { as {c₂,c₃} -> Element of Fin a₁;
coherence

proof end;

let c₄ be Element of c₁;
redefine func { as {c₂,c₃,c₄} -> Element of Fin a₁;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂, c₃ be Element of Fin c₁;
redefine func \/ as c₂ \/ c₃ -> Element of Fin a₁;
coherence by FINSUB_1:10;

end;

definition

let c₁ be set ;
let c₂, c₃ be Element of Fin c₁;
redefine func \ as c₂ \ c₃ -> Element of Fin a₁;
coherence by FINSUB_1:10;

end;

scheme :: SETWISEO:sch 2
s2{ F₁() -> non empty set , P₁[ set ] } :

for b₁ being Element of Fin F₁() holds P₁[b₁]

provided

E17: P₁[ {}. F₁()] and
E18: for b₁ being Element of Fin F₁()
for b₂ being Element of F₁() st P₁[b₁] & not b₂ in b₁ holds
P₁[b₁ \/ {b₂}]

proof end;

scheme :: SETWISEO:sch 3
s3{ F₁() -> non empty set , P₁[ Element of Fin F₁()] } :

for b₁ being Element of Fin F₁() st b₁ <> {} holds
P₁[b₁]

provided

E17: for b₁ being Element of F₁() holds P₁[{b₁}] and
E18: for b₁, b₂ being Element of Fin F₁() st b₁ <> {} & b₂ <> {} & P₁[b₁] & P₁[b₂] holds
P₁[b₁ \/ b₂]

proof end;

scheme :: SETWISEO:sch 4
s4{ F₁() -> non empty set , P₁[ set ] } :

for b₁ being Element of Fin F₁() holds P₁[b₁]

provided

E17: P₁[ {}. F₁()] and
E18: for b₁ being Element of Fin F₁()
for b₂ being Element of F₁() st P₁[b₁] holds
P₁[b₁ \/ {b₂}]

proof end;

definition

let c₁, c₂ be non empty set ;
let c₃ be BinOp of c₂;
let c₄ be Element of Fin c₁;
let c₅ be Function of c₁,c₂;
assume that
E17: ( c₄ <> {} or c₃ has_a_unity ) and
E18: c₃ is commutative and
E19: c₃ is associative ;
func c₃ $$ c₄,c₅ -> Element of a₂ means :Def3: :: SETWISEO:def 3
ex b₁ being Function of Fin a₁,a₂ st
( a₆ = b₁ . a₄ & ( for b₂ being Element of a₂ st b₂ is_a_unity_wrt a₃ holds
b₁ . {} = b₂ ) & ( for b₂ being Element of a₁ holds b₁ . {b₂} = a₅ . b₂ ) & ( for b₂ being Element of Fin a₁ st b₂ c= a₄ & b₂ <> {} holds
for b₃ being Element of a₁ st b₃ in a₄ \ b₂ holds
b₁ . (b₂ \/ {b₃}) = a₃ . (b₁ . b₂),(a₅ . b₃) ) );
existence

proof end;

uniqueness

proof end;

end;

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

theorem Th24: :: SETWISEO:24

canceled;

theorem Th25: :: SETWISEO:25

for b₁, b₂ being non empty set
for b₃ being BinOp of b₂
for b₄ being Element of Fin b₁
for b₅ being Function of b₁,b₂ st ( b₄ <> {} or b₃ has_a_unity ) & b₃ is idempotent & b₃ is commutative & b₃ is associative holds
for b₆ being Element of b₂ holds
( b₆ = b₃ $$ b₄,b₅ iff ex b₇ being Function of Fin b₁,b₂ st
( b₆ = b₇ . b₄ & ( for b₈ being Element of b₂ st b₈ is_a_unity_wrt b₃ holds
b₇ . {} = b₈ ) & ( for b₈ being Element of b₁ holds b₇ . {b₈} = b₅ . b₈ ) & ( for b₈ being Element of Fin b₁ st b₈ c= b₄ & b₈ <> {} holds
for b₉ being Element of b₁ st b₉ in b₄ holds
b₇ . (b₈ \/ {b₉}) = b₃ . (b₇ . b₈),(b₅ . b₉) ) ) )

proof end;

theorem Th26: :: SETWISEO:26

for b₁, b₂ being non empty set
for b₃ being BinOp of b₁
for b₄ being Function of b₂,b₁ st b₃ is commutative & b₃ is associative holds
for b₅ being Element of b₂ holds b₃ $$ {b₅},b₄ = b₄ . b₅

proof end;

theorem Th27: :: SETWISEO:27

for b₁, b₂ being non empty set
for b₃ being BinOp of b₁
for b₄ being Function of b₂,b₁ st b₃ is idempotent & b₃ is commutative & b₃ is associative holds
for b₅, b₆ being Element of b₂ holds b₃ $$ {b₅,b₆},b₄ = b₃ . (b₄ . b₅),(b₄ . b₆)

proof end;

theorem Th28: :: SETWISEO:28

for b₁, b₂ being non empty set
for b₃ being BinOp of b₁
for b₄ being Function of b₂,b₁ st b₃ is idempotent & b₃ is commutative & b₃ is associative holds
for b₅, b₆, b₇ being Element of b₂ holds b₃ $$ {b₅,b₆,b₇},b₄ = b₃ . (b₃ . (b₄ . b₅),(b₄ . b₆)),(b₄ . b₇)

proof end;

theorem Th29: :: SETWISEO:29

for b₁, b₂ being non empty set
for b₃ being BinOp of b₁
for b₄ being Element of Fin b₂
for b₅ being Function of b₂,b₁ st b₃ is idempotent & b₃ is commutative & b₃ is associative & b₄ <> {} holds
for b₆ being Element of b₂ holds b₃ $$ (b₄ \/ {b₆}),b₅ = b₃ . (b₃ $$ b₄,b₅),(b₅ . b₆)

proof end;

theorem Th30: :: SETWISEO:30

for b₁, b₂ being non empty set
for b₃ being BinOp of b₁
for b₄ being Function of b₂,b₁ st b₃ is idempotent & b₃ is commutative & b₃ is associative holds
for b₅, b₆ being Element of Fin b₂ st b₅ <> {} & b₆ <> {} holds
b₃ $$ (b₅ \/ b₆),b₄ = b₃ . (b₃ $$ b₅,b₄),(b₃ $$ b₆,b₄)

proof end;

theorem Th31: :: SETWISEO:31

for b₁, b₂ being non empty set
for b₃ being BinOp of b₁
for b₄ being Element of Fin b₂
for b₅ being Function of b₂,b₁ st b₃ is commutative & b₃ is associative & b₃ is idempotent holds
for b₆ being Element of b₂ st b₆ in b₄ holds
b₃ . (b₅ . b₆),(b₃ $$ b₄,b₅) = b₃ $$ b₄,b₅

proof end;

theorem Th32: :: SETWISEO:32

for b₁, b₂ being non empty set
for b₃ being BinOp of b₁
for b₄ being Function of b₂,b₁ st b₃ is commutative & b₃ is associative & b₃ is idempotent holds
for b₅, b₆ being Element of Fin b₂ st b₅ <> {} & b₅ c= b₆ holds
b₃ . (b₃ $$ b₅,b₄),(b₃ $$ b₆,b₄) = b₃ $$ b₆,b₄

proof end;

theorem Th33: :: SETWISEO:33

for b₁, b₂ being non empty set
for b₃ being BinOp of b₁
for b₄ being Element of Fin b₂
for b₅ being Function of b₂,b₁ st b₄ <> {} & b₃ is commutative & b₃ is associative & b₃ is idempotent holds
for b₆ being Element of b₁ st ( for b₇ being Element of b₂ st b₇ in b₄ holds
b₅ . b₇ = b₆ ) holds
b₃ $$ b₄,b₅ = b₆

proof end;

theorem Th34: :: SETWISEO:34

for b₁, b₂ being non empty set
for b₃ being BinOp of b₂
for b₄ being Element of Fin b₁
for b₅ being Function of b₁,b₂ st b₃ is commutative & b₃ is associative & b₃ is idempotent holds
for b₆ being Element of b₂ st b₅ .: b₄ = {b₆} holds
b₃ $$ b₄,b₅ = b₆

proof end;

theorem Th35: :: SETWISEO:35

for b₁, b₂ being non empty set
for b₃ being BinOp of b₂ st b₃ is commutative & b₃ is associative & b₃ is idempotent holds
for b₄, b₅ being Function of b₁,b₂
for b₆, b₇ being Element of Fin b₁ st b₆ <> {} & b₄ .: b₆ = b₅ .: b₇ holds
b₃ $$ b₆,b₄ = b₃ $$ b₇,b₅

proof end;

theorem Th36: :: SETWISEO:36

for b₁, b₂ being non empty set
for b₃, b₄ being BinOp of b₁ st b₃ is idempotent & b₃ is commutative & b₃ is associative & b₄ is_distributive_wrt b₃ holds
for b₅ being Element of Fin b₂ st b₅ <> {} holds
for b₆ being Function of b₂,b₁
for b₇ being Element of b₁ holds b₄ . b₇,(b₃ $$ b₅,b₆) = b₃ $$ b₅,(b₄ [;] b₇,b₆)

proof end;

theorem Th37: :: SETWISEO:37

for b₁, b₂ being non empty set
for b₃, b₄ being BinOp of b₁ st b₃ is idempotent & b₃ is commutative & b₃ is associative & b₄ is_distributive_wrt b₃ holds
for b₅ being Element of Fin b₂ st b₅ <> {} holds
for b₆ being Function of b₂,b₁
for b₇ being Element of b₁ holds b₄ . (b₃ $$ b₅,b₆),b₇ = b₃ $$ b₅,(b₄ [:] b₆,b₇)

proof end;

definition

let c₁, c₂ be non empty set ;
let c₃ be Function of c₁,c₂;
let c₄ be Element of Fin c₁;
redefine func .: as c₃ .: c₄ -> Element of Fin a₂;
coherence by Lemma11;

end;

theorem Th38: :: SETWISEO:38

for b₁, b₂, b₃ being non empty set
for b₄ being BinOp of b₁ st b₄ is idempotent & b₄ is commutative & b₄ is associative holds
for b₅ being Element of Fin b₂ st b₅ <> {} holds
for b₆ being Function of b₂,b₃
for b₇ being Function of b₃,b₁ holds b₄ $$ (b₆ .: b₅),b₇ = b₄ $$ b₅,(b₇ * b₆)

proof end;

theorem Th39: :: SETWISEO:39

for b₁, b₂ being non empty set
for b₃ being BinOp of b₂ st b₃ is commutative & b₃ is associative & b₃ is idempotent holds
for b₄ being non empty set
for b₅ being BinOp of b₄ st b₅ is commutative & b₅ is associative & b₅ is idempotent holds
for b₆ being Function of b₁,b₂
for b₇ being Function of b₂,b₄ st ( for b₈, b₉ being Element of b₂ holds b₇ . (b₃ . b₈,b₉) = b₅ . (b₇ . b₈),(b₇ . b₉) ) holds
for b₈ being Element of Fin b₁ st b₈ <> {} holds
b₇ . (b₃ $$ b₈,b₆) = b₅ $$ b₈,(b₇ * b₆)

proof end;

theorem Th40: :: SETWISEO:40

for b₁, b₂ being non empty set
for b₃ being BinOp of b₁ st b₃ is commutative & b₃ is associative & b₃ has_a_unity holds
for b₄ being Function of b₂,b₁ holds b₃ $$ ({}. b₂),b₄ = the_unity_wrt b₃

proof end;

theorem Th41: :: SETWISEO:41

for b₁, b₂ being non empty set
for b₃ being BinOp of b₁
for b₄ being Element of Fin b₂
for b₅ being Function of b₂,b₁ st b₃ is idempotent & b₃ is commutative & b₃ is associative & b₃ has_a_unity holds
for b₆ being Element of b₂ holds b₃ $$ (b₄ \/ {b₆}),b₅ = b₃ . (b₃ $$ b₄,b₅),(b₅ . b₆)

proof end;

theorem Th42: :: SETWISEO:42

for b₁, b₂ being non empty set
for b₃ being BinOp of b₁
for b₄ being Function of b₂,b₁ st b₃ is idempotent & b₃ is commutative & b₃ is associative & b₃ has_a_unity holds
for b₅, b₆ being Element of Fin b₂ holds b₃ $$ (b₅ \/ b₆),b₄ = b₃ . (b₃ $$ b₅,b₄),(b₃ $$ b₆,b₄)

proof end;

theorem Th43: :: SETWISEO:43

for b₁, b₂ being non empty set
for b₃ being BinOp of b₂ st b₃ is commutative & b₃ is associative & b₃ is idempotent & b₃ has_a_unity holds
for b₄, b₅ being Function of b₁,b₂
for b₆, b₇ being Element of Fin b₁ st b₄ .: b₆ = b₅ .: b₇ holds
b₃ $$ b₆,b₄ = b₃ $$ b₇,b₅

proof end;

theorem Th44: :: SETWISEO:44

for b₁, b₂, b₃ being non empty set
for b₄ being BinOp of b₁ st b₄ is idempotent & b₄ is commutative & b₄ is associative & b₄ has_a_unity holds
for b₅ being Element of Fin b₂
for b₆ being Function of b₂,b₃
for b₇ being Function of b₃,b₁ holds b₄ $$ (b₆ .: b₅),b₇ = b₄ $$ b₅,(b₇ * b₆)

proof end;

theorem Th45: :: SETWISEO:45

for b₁, b₂ being non empty set
for b₃ being BinOp of b₂ st b₃ is commutative & b₃ is associative & b₃ is idempotent & b₃ has_a_unity holds
for b₄ being non empty set
for b₅ being BinOp of b₄ st b₅ is commutative & b₅ is associative & b₅ is idempotent & b₅ has_a_unity holds
for b₆ being Function of b₁,b₂
for b₇ being Function of b₂,b₄ st b₇ . (the_unity_wrt b₃) = the_unity_wrt b₅ & ( for b₈, b₉ being Element of b₂ holds b₇ . (b₃ . b₈,b₉) = b₅ . (b₇ . b₈),(b₇ . b₉) ) holds
for b₈ being Element of Fin b₁ holds b₇ . (b₃ $$ b₈,b₆) = b₅ $$ b₈,(b₇ * b₆)

proof end;

definition

let c₁ be set ;
func FinUnion c₁ -> BinOp of Fin a₁ means :Def4: :: SETWISEO:def 4
for b₁, b₂ being Element of Fin a₁ holds a₂ . b₁,b₂ = b₁ \/ b₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines FinUnion SETWISEO:def 4 :

theorem Th46: :: SETWISEO:46

canceled;

theorem Th47: :: SETWISEO:47

canceled;

theorem Th48: :: SETWISEO:48

canceled;

theorem Th49: :: SETWISEO:49

for b₁ being set holds FinUnion b₁ is idempotent

proof end;

theorem Th50: :: SETWISEO:50

for b₁ being set holds FinUnion b₁ is commutative

proof end;

theorem Th51: :: SETWISEO:51

for b₁ being set holds FinUnion b₁ is associative

proof end;

theorem Th52: :: SETWISEO:52

for b₁ being set holds {}. b₁ is_a_unity_wrt FinUnion b₁

proof end;

theorem Th53: :: SETWISEO:53

for b₁ being set holds FinUnion b₁ has_a_unity

proof end;

theorem Th54: :: SETWISEO:54

for b₁ being set holds the_unity_wrt (FinUnion b₁) is_a_unity_wrt FinUnion b₁

proof end;

theorem Th55: :: SETWISEO:55

for b₁ being set holds the_unity_wrt (FinUnion b₁) = {}

proof end;

definition

let c₁ be non empty set ;
let c₂ be set ;
let c₃ be Element of Fin c₁;
let c₄ be Function of c₁, Fin c₂;
func FinUnion c₃,c₄ -> Element of Fin a₂ equals :: SETWISEO:def 5
(FinUnion a₂) $$ a₃,a₄;
coherence ;

end;

:: deftheorem Def5 defines FinUnion SETWISEO:def 5 :

theorem Th56: :: SETWISEO:56

for b₁ being non empty set
for b₂ being set
for b₃ being Function of b₁, Fin b₂
for b₄ being Element of b₁ holds FinUnion {b₄},b₃ = b₃ . b₄

proof end;

theorem Th57: :: SETWISEO:57

for b₁ being non empty set
for b₂ being set
for b₃ being Function of b₁, Fin b₂
for b₄, b₅ being Element of b₁ holds FinUnion {b₄,b₅},b₃ = (b₃ . b₄) \/ (b₃ . b₅)

proof end;

theorem Th58: :: SETWISEO:58

for b₁ being non empty set
for b₂ being set
for b₃ being Function of b₁, Fin b₂
for b₄, b₅, b₆ being Element of b₁ holds FinUnion {b₄,b₅,b₆},b₃ = ((b₃ . b₄) \/ (b₃ . b₅)) \/ (b₃ . b₆)

proof end;

theorem Th59: :: SETWISEO:59

for b₁ being non empty set
for b₂ being set
for b₃ being Function of b₁, Fin b₂ holds FinUnion ({}. b₁),b₃ = {}

proof end;

theorem Th60: :: SETWISEO:60

for b₁ being non empty set
for b₂ being set
for b₃ being Function of b₁, Fin b₂
for b₄ being Element of b₁
for b₅ being Element of Fin b₁ holds FinUnion (b₅ \/ {b₄}),b₃ = (FinUnion b₅,b₃) \/ (b₃ . b₄)

proof end;

theorem Th61: :: SETWISEO:61

for b₁ being non empty set
for b₂ being set
for b₃ being Function of b₁, Fin b₂
for b₄ being Element of Fin b₁ holds FinUnion b₄,b₃ = union (b₃ .: b₄)

proof end;

theorem Th62: :: SETWISEO:62

for b₁ being non empty set
for b₂ being set
for b₃ being Function of b₁, Fin b₂
for b₄, b₅ being Element of Fin b₁ holds FinUnion (b₄ \/ b₅),b₃ = (FinUnion b₄,b₃) \/ (FinUnion b₅,b₃)

proof end;

theorem Th63: :: SETWISEO:63

for b₁, b₂ being non empty set
for b₃ being set
for b₄ being Element of Fin b₁
for b₅ being Function of b₁,b₂
for b₆ being Function of b₂, Fin b₃ holds FinUnion (b₅ .: b₄),b₆ = FinUnion b₄,(b₆ * b₅)

proof end;

theorem Th64: :: SETWISEO:64

for b₁, b₂ being non empty set
for b₃ being set
for b₄ being BinOp of b₁ st b₄ is commutative & b₄ is associative & b₄ is idempotent holds
for b₅ being Element of Fin b₂ st b₅ <> {} holds
for b₆ being Function of b₂, Fin b₃
for b₇ being Function of Fin b₃,b₁ st ( for b₈, b₉ being Element of Fin b₃ holds b₇ . (b₈ \/ b₉) = b₄ . (b₇ . b₈),(b₇ . b₉) ) holds
b₇ . (FinUnion b₅,b₆) = b₄ $$ b₅,(b₇ * b₆)

proof end;

theorem Th65: :: SETWISEO:65

for b₁, b₂ being non empty set
for b₃ being set
for b₄ being BinOp of b₂ st b₄ is commutative & b₄ is associative & b₄ is idempotent & b₄ has_a_unity holds
for b₅ being Function of b₁, Fin b₃
for b₆ being Function of Fin b₃,b₂ st b₆ . ({}. b₃) = the_unity_wrt b₄ & ( for b₇, b₈ being Element of Fin b₃ holds b₆ . (b₇ \/ b₈) = b₄ . (b₆ . b₇),(b₆ . b₈) ) holds
for b₇ being Element of Fin b₁ holds b₆ . (FinUnion b₇,b₅) = b₄ $$ b₇,(b₆ * b₅)

proof end;

definition

let c₁ be set ;
func singleton c₁ -> Function of a₁, Fin a₁ means :Def6: :: SETWISEO:def 6
for b₁ being set st b₁ in a₁ holds
a₂ . b₁ = {b₁};
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines singleton SETWISEO:def 6 :

theorem Th66: :: SETWISEO:66

canceled;

theorem Th67: :: SETWISEO:67

for b₁ being non empty set
for b₂ being Function of b₁, Fin b₁ holds
( b₂ = singleton b₁ iff for b₃ being Element of b₁ holds b₂ . b₃ = {b₃} )

proof end;

theorem Th68: :: SETWISEO:68

for b₁ being non empty set
for b₂ being set
for b₃ being Element of b₁ holds
( b₂ in (singleton b₁) . b₃ iff b₂ = b₃ )

proof end;

theorem Th69: :: SETWISEO:69

for b₁ being non empty set
for b₂, b₃, b₄ being Element of b₁ st b₂ in (singleton b₁) . b₄ & b₃ in (singleton b₁) . b₄ holds
b₂ = b₃

proof end;

Lemma47: for b₁ being non empty set
for b₂, b₃ being set
for b₄ being Function of b₂,b₁ holds b₄ .: b₃ c= b₁
;

theorem Th70: :: SETWISEO:70

for b₁ being non empty set
for b₂ being set
for b₃ being Function of b₁, Fin b₂
for b₄ being Element of Fin b₁
for b₅ being set holds
( b₅ in FinUnion b₄,b₃ iff ex b₆ being Element of b₁ st
( b₆ in b₄ & b₅ in b₃ . b₆ ) )

proof end;

theorem Th71: :: SETWISEO:71

for b₁ being non empty set
for b₂ being Element of Fin b₁ holds FinUnion b₂,(singleton b₁) = b₂

proof end;

theorem Th72: :: SETWISEO:72

for b₁ being non empty set
for b₂, b₃ being set
for b₄ being Function of b₁, Fin b₂
for b₅ being Function of Fin b₂, Fin b₃ st b₅ . ({}. b₂) = {}. b₃ & ( for b₆, b₇ being Element of Fin b₂ holds b₅ . (b₆ \/ b₇) = (b₅ . b₆) \/ (b₅ . b₇) ) holds
for b₆ being Element of Fin b₁ holds b₅ . (FinUnion b₆,b₄) = FinUnion b₆,(b₅ * b₄)

proof end;