:: SETWISEO semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem :: SETWISEO:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: SETWISEO:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th3: :: SETWISEO:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being set holds {x} c= {x,y,z}
proof end;

theorem Th4: :: SETWISEO:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being set holds {x,y} c= {x,y,z}
proof end;

theorem Th5: :: SETWISEO:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y, x being set holds
( not X c= Y \/ {x} or x in X or X c= Y )
proof end;

theorem Th6: :: SETWISEO:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, X, y being set holds
( x in X \/ {y} iff ( x in X or x = y ) )
proof end;

theorem :: SETWISEO:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th8: :: SETWISEO:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, x, Y being set holds
( X \/ {x} c= Y iff ( x in Y & X c= Y ) )
proof end;

theorem :: SETWISEO:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: SETWISEO:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th11: :: SETWISEO:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set
for f being Function holds f .: (Y \ (f " X)) = (f .: Y) \ X
proof end;

theorem Th12: :: SETWISEO:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)}
proof end;

theorem Th13: :: SETWISEO:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y, X being non empty set
for f being Function of X,Y
for x being Element of X holds f .: {x} = {(f . x)}
proof end;

theorem Th14: :: SETWISEO:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: SETWISEO:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th16: :: SETWISEO:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for B being Element of Fin X
for A being set st A c= B holds
A is Element of Fin X
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 :: SETWISEO:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th18: :: SETWISEO:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th19: :: SETWISEO:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 = {}
proof end;

registration
let X be set ;
cluster empty Element of Fin X;
existence
ex b1 being Element of Fin X st b1 is empty
proof end;
end;

definition
let X be set ;
func {}. X -> empty Element of Fin X equals :: SETWISEO:def 1
{} ;
coherence
{} is empty Element of Fin X
by FINSUB_1:18;
end;

:: deftheorem defines {}. SETWISEO:def 1 :
for X being set holds {}. X = {} ;

scheme :: SETWISEO:sch 1
FinSubFuncEx{ F1() -> non empty set , F2() -> Element of Fin F1(), P1[ set , set ] } :
ex f being Function of F1(), Fin F1() st
for b, a being Element of F1() holds
( a in f . b iff ( a in F2() & P1[a,b] ) )
proof end;

definition
let X be non empty set ;
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;
end;

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

notation
let X be non empty set ;
let F be BinOp of X;
synonym F has_a_unity for having_a_unity F;
end;

theorem :: SETWISEO:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: SETWISEO:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th22: :: SETWISEO:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for F being BinOp of X holds
( F has_a_unity iff the_unity_wrt F is_a_unity_wrt F )
proof end;

theorem Th23: :: SETWISEO:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for F being BinOp of X st F has_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;

registration
let X be non empty set ;
cluster non empty Element of Fin X;
existence
not for b1 being Element of Fin X holds b1 is empty
proof end;
end;

definition
let X be non empty set ;
let x be Element of X;
:: original: {
redefine func {x} -> Element of Fin X;
coherence
{x} is Element of Fin X
proof end;
let y be Element of X;
:: original: {
redefine func {x,y} -> Element of Fin X;
coherence
{x,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
{x,y,z} is Element of Fin X
proof end;
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:10;
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:10;
end;

scheme :: SETWISEO:sch 2
FinSubInd1{ F1() -> non empty set , P1[ set ] } :
for B being Element of Fin F1() holds P1[B]
provided
A1: P1[ {}. F1()] and
A2: for B' being Element of Fin F1()
for b being Element of F1() st P1[B'] & not b in B' holds
P1[B' \/ {b}]
proof end;

scheme :: SETWISEO:sch 3
FinSubInd2{ F1() -> non empty set , P1[ Element of Fin F1()] } :
for B being Element of Fin F1() st B <> {} holds
P1[B]
provided
A1: for x being Element of F1() holds P1[{x}] and
A2: for B1, B2 being Element of Fin F1() st B1 <> {} & B2 <> {} & P1[B1] & P1[B2] holds
P1[B1 \/ B2]
proof end;

scheme :: SETWISEO:sch 4
FinSubInd3{ F1() -> non empty set , P1[ set ] } :
for B being Element of Fin F1() holds P1[B]
provided
A1: P1[ {}. F1()] and
A2: for B' being Element of Fin F1()
for b being Element of F1() st P1[B'] holds
P1[B' \/ {b}]
proof end;

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 has_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 B' being Element of Fin X st B' c= B & B' <> {} holds
for x being Element of X st x in B \ B' holds
G . (B' \/ {x}) = F . (G . B'),(f . x) ) );
existence
ex b1 being Element of Y ex G being Function of Fin X,Y st
( b1 = 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 B' being Element of Fin X st B' c= B & B' <> {} holds
for x being Element of X st x in B \ B' holds
G . (B' \/ {x}) = F . (G . B'),(f . x) ) )
proof end;
uniqueness
for b1, b2 being Element of Y st ex G being Function of Fin X,Y st
( b1 = 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 B' being Element of Fin X st B' c= B & B' <> {} holds
for x being Element of X st x in B \ B' holds
G . (B' \/ {x}) = F . (G . B'),(f . x) ) ) & ex G being Function of Fin X,Y st
( b2 = 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 B' being Element of Fin X st B' c= B & B' <> {} holds
for x being Element of X st x in B \ B' holds
G . (B' \/ {x}) = F . (G . B'),(f . x) ) ) holds
b1 = b2
proof end;
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 has_a_unity ) & F is commutative & F is associative holds
for b6 being Element of Y holds
( b6 = F $$ B,f iff ex G being Function of Fin X,Y st
( b6 = 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 B' being Element of Fin X st B' c= B & B' <> {} holds
for x being Element of X st x in B \ B' holds
G . (B' \/ {x}) = F . (G . B'),(f . x) ) ) );

theorem :: SETWISEO:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th25: :: SETWISEO:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 has_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 B' being Element of Fin X st B' c= B & B' <> {} holds
for x being Element of X st x in B holds
G . (B' \/ {x}) = F . (G . B'),(f . x) ) ) )
proof end;

theorem Th26: :: SETWISEO:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th27: :: SETWISEO:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th28: :: SETWISEO:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th29: :: SETWISEO:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th30: :: SETWISEO:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem :: SETWISEO:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: SETWISEO:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th33: :: SETWISEO:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th34: :: SETWISEO:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th35: :: SETWISEO:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: SETWISEO:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem :: SETWISEO:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
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;

theorem Th38: :: SETWISEO:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th39: :: SETWISEO:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th40: :: SETWISEO:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y, X being non empty set
for F being BinOp of Y st F is commutative & F is associative & F has_a_unity holds
for f being Function of X,Y holds F $$ ({}. X),f = the_unity_wrt F
proof end;

theorem Th41: :: SETWISEO:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 has_a_unity holds
for x being Element of X holds F $$ (B \/ {x}),f = F . (F $$ B,f),(f . x)
proof end;

theorem :: SETWISEO:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 has_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:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty set
for F being BinOp of Y st F is commutative & F is associative & F is idempotent & F has_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 Th44: :: SETWISEO:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 has_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:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty set
for F being BinOp of Y st F is commutative & F is associative & F is idempotent & F has_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 has_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 ;
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
ex b1 being BinOp of Fin A st
for x, y being Element of Fin A holds b1 . x,y = x \/ y
proof end;
uniqueness
for b1, b2 being BinOp of Fin A st ( for x, y being Element of Fin A holds b1 . x,y = x \/ y ) & ( for x, y being Element of Fin A holds b2 . x,y = x \/ y ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines FinUnion SETWISEO:def 4 :
for A being set
for b2 being BinOp of Fin A holds
( b2 = FinUnion A iff for x, y being Element of Fin A holds b2 . x,y = x \/ y );

theorem :: SETWISEO:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: SETWISEO:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: SETWISEO:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th49: :: SETWISEO:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being set holds FinUnion A is idempotent
proof end;

theorem Th50: :: SETWISEO:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being set holds FinUnion A is commutative
proof end;

theorem Th51: :: SETWISEO:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being set holds FinUnion A is associative
proof end;

theorem Th52: :: SETWISEO:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being set holds {}. A is_a_unity_wrt FinUnion A
proof end;

theorem Th53: :: SETWISEO:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being set holds FinUnion A has_a_unity
proof end;

theorem :: SETWISEO:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being set holds the_unity_wrt (FinUnion A) is_a_unity_wrt FinUnion A
proof end;

theorem Th55: :: SETWISEO:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being set holds the_unity_wrt (FinUnion A) = {}
proof end;

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;
func FinUnion B,f -> Element of Fin A equals :: SETWISEO:def 5
(FinUnion A) $$ B,f;
coherence
(FinUnion A) $$ B,f is Element of Fin A
;
end;

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

theorem :: SETWISEO:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: SETWISEO:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem :: SETWISEO:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th59: :: SETWISEO:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for A being set
for f being Function of X, Fin A holds FinUnion ({}. X),f = {}
proof end;

theorem Th60: :: SETWISEO:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th61: :: SETWISEO:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem :: SETWISEO:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem :: SETWISEO:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th64: :: SETWISEO:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th65: :: SETWISEO:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 has_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 ;
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
ex b1 being Function of A, Fin A st
for x being set st x in A holds
b1 . x = {x}
proof end;
uniqueness
for b1, b2 being Function of A, Fin A st ( for x being set st x in A holds
b1 . x = {x} ) & ( for x being set st x in A holds
b2 . x = {x} ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines singleton SETWISEO:def 6 :
for A being set
for b2 being Function of A, Fin A holds
( b2 = singleton A iff for x being set st x in A holds
b2 . x = {x} );

theorem :: SETWISEO:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th67: :: SETWISEO:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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} )
proof end;

theorem Th68: :: SETWISEO:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem :: SETWISEO:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
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 Th70: :: SETWISEO:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) )
proof end;

theorem :: SETWISEO:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for B being Element of Fin X holds FinUnion B,(singleton X) = B
proof end;

theorem :: SETWISEO:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;