begin
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 Th36:
for
x,
A,
X being
set st
(chi (A,X)) . x = 1 holds
x in A
theorem
for
A,
X,
B being
set st
A c= X &
B c= X &
chi (
A,
X)
= chi (
B,
X) holds
A = B
definition
let X,
Y be
set ;
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
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;
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;
definition
let f,
g be
Function;
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;
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 Th74;
end;
begin