begin
theorem Th1:
theorem
theorem
begin
:: deftheorem Def1 defines { PZFMISC1:def 1 :
for I being set
for A, b3 being ManySortedSet of I holds
( b3 = {A} iff for i being set st i in I holds
b3 . i = {(A . i)} );
definition
let I be
set ;
let A,
B be
ManySortedSet of
I;
func {A,B} -> ManySortedSet of
I means :
Def2:
for
i being
set st
i in I holds
it . i = {(A . i),(B . i)};
existence
ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i = {(A . i),(B . i)}
uniqueness
for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = {(A . i),(B . i)} ) & ( for i being set st i in I holds
b2 . i = {(A . i),(B . i)} ) holds
b1 = b2
commutativity
for b1, A, B being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = {(A . i),(B . i)} ) holds
for i being set st i in I holds
b1 . i = {(B . i),(A . i)}
;
end;
:: deftheorem Def2 defines { PZFMISC1:def 2 :
for I being set
for A, B, b4 being ManySortedSet of I holds
( b4 = {A,B} iff for i being set st i in I holds
b4 . i = {(A . i),(B . i)} );
theorem
theorem
theorem
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
begin
theorem
theorem
theorem
theorem
theorem
theorem
theorem
begin
theorem
theorem
theorem
theorem
theorem
begin
theorem
theorem
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
theorem
theorem
begin
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
for
I being
set for
x,
y,
X being
ManySortedSet of
I holds
(
[|{x,y},X|] = [|{x},X|] \/ [|{y},X|] &
[|X,{x,y}|] = [|X,{x}|] \/ [|X,{y}|] )
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
begin
:: deftheorem defines is_transformable_to PZFMISC1:def 3 :
for I being set
for A, B being ManySortedSet of I holds
( A is_transformable_to B iff for i being set st i in I & B . i = {} holds
A . i = {} );