begin
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
scheme
FuncEx3{
F1()
-> set ,
F2()
-> set ,
P1[
set ,
set ,
set ] } :
ex
f being
Function st
(
dom f = [:F1(),F2():] & ( for
x,
y being
set st
x in F1() &
y in F2() holds
P1[
x,
y,
f . x,
y] ) )
provided
A1:
for
x,
y,
z1,
z2 being
set st
x in F1() &
y in F2() &
P1[
x,
y,
z1] &
P1[
x,
y,
z2] holds
z1 = z2
and A2:
for
x,
y being
set st
x in F1() &
y in F2() holds
ex
z being
set st
P1[
x,
y,
z]
theorem Th6:
:: deftheorem Def1 defines .: FUNCT_3:def 1 :
theorem
canceled;
theorem Th8:
theorem
theorem Th10:
theorem
canceled;
theorem
theorem Th13:
theorem
theorem Th15:
theorem Th16:
theorem
theorem Th18:
theorem
theorem
theorem Th21:
theorem Th22:
:: deftheorem Def2 defines " FUNCT_3:def 2 :
theorem
canceled;
theorem Th24:
theorem Th25:
theorem
canceled;
theorem
theorem
theorem Th29:
theorem
theorem Th31:
theorem
theorem Th33:
theorem
theorem Th35:
theorem Th36:
theorem
theorem
theorem
:: deftheorem Def3 defines chi FUNCT_3:def 3 :
for
A,
X being
set for
b3 being
Function holds
(
b3 = chi A,
X iff (
dom b3 = X & ( for
x being
set st
x in X holds
( (
x in A implies
b3 . x = 1 ) & ( not
x in A implies
b3 . x = {} ) ) ) ) );
theorem
canceled;
theorem
canceled;
theorem Th42:
for
x,
A,
X being
set st
(chi A,X) . x = 1 holds
x in A
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem Th48:
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem
canceled;
theorem
definition
let X,
Y be
set ;
canceled;func pr1 X,
Y -> Function means :
Def5:
(
dom it = [:X,Y:] & ( for
x,
y being
set st
x in X &
y in Y holds
it . x,
y = x ) );
existence
ex b1 being Function st
( dom b1 = [:X,Y:] & ( for x, y being set st x in X & y in Y holds
b1 . x,y = x ) )
uniqueness
for b1, b2 being Function st dom b1 = [:X,Y:] & ( for x, y being set st x in X & y in Y holds
b1 . x,y = x ) & dom b2 = [:X,Y:] & ( for x, y being set st x in X & y in Y holds
b2 . x,y = x ) holds
b1 = b2
func pr2 X,
Y -> Function means :
Def6:
(
dom it = [:X,Y:] & ( for
x,
y being
set st
x in X &
y in Y holds
it . x,
y = y ) );
existence
ex b1 being Function st
( dom b1 = [:X,Y:] & ( for x, y being set st x in X & y in Y holds
b1 . x,y = y ) )
uniqueness
for b1, b2 being Function st dom b1 = [:X,Y:] & ( for x, y being set st x in X & y in Y holds
b1 . x,y = y ) & dom b2 = [:X,Y:] & ( for x, y being set st x in X & y in Y holds
b2 . x,y = y ) holds
b1 = b2
end;
:: deftheorem FUNCT_3:def 4 :
canceled;
:: deftheorem Def5 defines pr1 FUNCT_3:def 5 :
:: deftheorem Def6 defines pr2 FUNCT_3:def 6 :
theorem
canceled;
theorem
canceled;
theorem Th59:
theorem
theorem Th61:
theorem
definition
let X,
Y be
set ;
pr1redefine func pr1 X,
Y -> Function of
[:X,Y:],
X;
coherence
pr1 X,Y is Function of [:X,Y:],X
pr2redefine func pr2 X,
Y -> Function of
[:X,Y:],
Y;
coherence
pr2 X,Y is Function of [:X,Y:],Y
end;
:: deftheorem Def7 defines delta FUNCT_3:def 7 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th66:
:: deftheorem Def8 defines <: FUNCT_3:def 8 :
theorem
canceled;
theorem Th68:
theorem Th69:
theorem Th70:
theorem Th71:
theorem Th72:
theorem Th73:
theorem Th74:
theorem
theorem
theorem
theorem Th78:
theorem
theorem
theorem Th81:
theorem
theorem
theorem
definition
let f,
g be
Function;
func [:f,g:] -> Function means :
Def9:
(
dom it = [:(dom f),(dom g):] & ( for
x,
y being
set st
x in dom f &
y in dom g holds
it . x,
y = [(f . x),(g . y)] ) );
existence
ex b1 being Function st
( dom b1 = [:(dom f),(dom g):] & ( for x, y being set st x in dom f & y in dom g holds
b1 . x,y = [(f . x),(g . y)] ) )
uniqueness
for b1, b2 being Function st dom b1 = [:(dom f),(dom g):] & ( for x, y being set st x in dom f & y in dom g holds
b1 . x,y = [(f . x),(g . y)] ) & dom b2 = [:(dom f),(dom g):] & ( for x, y being set st x in dom f & y in dom g holds
b2 . x,y = [(f . x),(g . y)] ) holds
b1 = b2
end;
:: deftheorem Def9 defines [: FUNCT_3:def 9 :
theorem
canceled;
theorem Th86:
theorem Th87:
theorem Th88:
theorem Th89:
theorem
theorem
theorem
theorem
theorem
theorem Th95:
definition
let X1,
X2,
Y1,
Y2 be
set ;
let f1 be
Function of
X1,
Y1;
let f2 be
Function of
X2,
Y2;
[:redefine func [:f1,f2:] -> Function of
[:X1,X2:],
[:Y1,Y2:];
coherence
[:f1,f2:] is Function of [:X1,X2:],[:Y1,Y2:]
by Th95;
end;
theorem
theorem
theorem
theorem
begin
theorem