begin
Lm1:
for x, y, Z being set st [x,y] in Z holds
( x in union (union Z) & y in union (union Z) )
Lm2:
for x, x', y, y', x1, x1', y1, y1' being set st [[x,x'],[y,y']] = [[x1,x1'],[y1,y1']] holds
( x = x1 & y = y1 & x' = x1' & y' = y1' )
theorem Th1:
for
Z being
set st ( for
z being
set st
z in Z holds
ex
x,
y being
set st
z = [x,y] ) holds
ex
X,
Y being
set st
Z c= [:X,Y:]
theorem
theorem
canceled;
theorem
theorem
theorem Th6:
theorem
theorem
theorem
theorem
:: deftheorem Def1 defines +* FUNCT_4:def 1 :
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem
theorem Th18:
theorem
theorem Th20:
theorem Th21:
theorem Th22:
theorem
theorem
theorem Th25:
theorem Th26:
theorem
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem
theorem Th35:
theorem
theorem
theorem Th38:
theorem
theorem
theorem
definition
let f be
Function;
func ~ f -> Function means :
Def2:
( ( for
x being
set holds
(
x in dom it iff ex
y,
z being
set st
(
x = [z,y] &
[y,z] in dom f ) ) ) & ( for
y,
z being
set st
[y,z] in dom f holds
it . z,
y = f . y,
z ) );
existence
ex b1 being Function st
( ( for x being set holds
( x in dom b1 iff ex y, z being set st
( x = [z,y] & [y,z] in dom f ) ) ) & ( for y, z being set st [y,z] in dom f holds
b1 . z,y = f . y,z ) )
uniqueness
for b1, b2 being Function st ( for x being set holds
( x in dom b1 iff ex y, z being set st
( x = [z,y] & [y,z] in dom f ) ) ) & ( for y, z being set st [y,z] in dom f holds
b1 . z,y = f . y,z ) & ( for x being set holds
( x in dom b2 iff ex y, z being set st
( x = [z,y] & [y,z] in dom f ) ) ) & ( for y, z being set st [y,z] in dom f holds
b2 . z,y = f . y,z ) holds
b1 = b2
end;
:: deftheorem Def2 defines ~ FUNCT_4:def 2 :
theorem Th42:
theorem Th43:
theorem
theorem
theorem Th46:
theorem Th47:
theorem Th48:
theorem
theorem Th50:
theorem
theorem Th52:
theorem Th53:
theorem
theorem
canceled;
theorem
canceled;
definition
let f,
g be
Function;
func |:f,g:| -> Function means :
Def3:
( ( for
z being
set holds
(
z in dom it iff ex
x,
y,
x',
y' being
set st
(
z = [[x,x'],[y,y']] &
[x,y] in dom f &
[x',y'] in dom g ) ) ) & ( for
x,
y,
x',
y' being
set st
[x,y] in dom f &
[x',y'] in dom g holds
it . [x,x'],
[y,y'] = [(f . x,y),(g . x',y')] ) );
existence
ex b1 being Function st
( ( for z being set holds
( z in dom b1 iff ex x, y, x', y' being set st
( z = [[x,x'],[y,y']] & [x,y] in dom f & [x',y'] in dom g ) ) ) & ( for x, y, x', y' being set st [x,y] in dom f & [x',y'] in dom g holds
b1 . [x,x'],[y,y'] = [(f . x,y),(g . x',y')] ) )
uniqueness
for b1, b2 being Function st ( for z being set holds
( z in dom b1 iff ex x, y, x', y' being set st
( z = [[x,x'],[y,y']] & [x,y] in dom f & [x',y'] in dom g ) ) ) & ( for x, y, x', y' being set st [x,y] in dom f & [x',y'] in dom g holds
b1 . [x,x'],[y,y'] = [(f . x,y),(g . x',y')] ) & ( for z being set holds
( z in dom b2 iff ex x, y, x', y' being set st
( z = [[x,x'],[y,y']] & [x,y] in dom f & [x',y'] in dom g ) ) ) & ( for x, y, x', y' being set st [x,y] in dom f & [x',y'] in dom g holds
b2 . [x,x'],[y,y'] = [(f . x,y),(g . x',y')] ) holds
b1 = b2
end;
:: deftheorem Def3 defines |: FUNCT_4:def 3 :
for
f,
g,
b3 being
Function holds
(
b3 = |:f,g:| iff ( ( for
z being
set holds
(
z in dom b3 iff ex
x,
y,
x',
y' being
set st
(
z = [[x,x'],[y,y']] &
[x,y] in dom f &
[x',y'] in dom g ) ) ) & ( for
x,
y,
x',
y' being
set st
[x,y] in dom f &
[x',y'] in dom g holds
b3 . [x,x'],
[y,y'] = [(f . x,y),(g . x',y')] ) ) );
theorem Th57:
for
x,
x',
y,
y' being
set for
f,
g being
Function holds
(
[[x,x'],[y,y']] in dom |:f,g:| iff (
[x,y] in dom f &
[x',y'] in dom g ) )
theorem
for
x,
x',
y,
y' being
set for
f,
g being
Function st
[[x,x'],[y,y']] in dom |:f,g:| holds
|:f,g:| . [x,x'],
[y,y'] = [(f . x,y),(g . x',y')]
theorem Th59:
theorem Th60:
for
X,
Y,
X',
Y' being
set for
f,
g being
Function st
dom f c= [:X,Y:] &
dom g c= [:X',Y':] holds
dom |:f,g:| c= [:[:X,X':],[:Y,Y':]:]
theorem Th61:
for
X,
Y,
X',
Y' being
set for
f,
g being
Function st
dom f = [:X,Y:] &
dom g = [:X',Y':] holds
dom |:f,g:| = [:[:X,X':],[:Y,Y':]:]
theorem
theorem Th63:
for
X,
Y,
Z,
X',
Y',
Z' being
set for
f being
Function of
[:X,Y:],
Z for
g being
Function of
[:X',Y':],
Z' st
Z <> {} &
Z' <> {} holds
|:f,g:| is
Function of
[:[:X,X':],[:Y,Y':]:],
[:Z,Z':]
theorem
for
X,
Y,
X',
Y' being
set for
D,
D' being non
empty set for
f being
Function of
[:X,Y:],
D for
g being
Function of
[:X',Y':],
D' holds
|:f,g:| is
Function of
[:[:X,X':],[:Y,Y':]:],
[:D,D':] by Th63;
:: deftheorem defines --> FUNCT_4:def 4 :
theorem Th65:
theorem Th66:
for
x1,
x2,
y1,
y2 being
set holds
( (
x1 <> x2 implies
(x1,x2 --> y1,y2) . x1 = y1 ) &
(x1,x2 --> y1,y2) . x2 = y2 )
theorem
for
x1,
x2,
y1,
y2 being
set st
x1 <> x2 holds
rng (x1,x2 --> y1,y2) = {y1,y2}
theorem
definition
let A be non
empty set ;
let x1,
x2 be
set ;
let y1,
y2 be
Element of
A;
-->redefine func x1,
x2 --> y1,
y2 -> Function of
{x1,x2},
A;
coherence
x1,x2 --> y1,y2 is Function of {x1,x2},A
end;
theorem
theorem
canceled;
theorem Th71:
theorem
for
a,
b,
x,
y,
x',
y' being
set st
a <> b &
a,
b --> x,
y = a,
b --> x',
y' holds
(
x = x' &
y = y' )
begin
theorem
theorem Th74:
theorem Th75:
theorem Th76:
theorem
theorem
theorem Th79:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th90:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th102:
theorem
theorem Th104:
begin
:: deftheorem defines +~ FUNCT_4:def 5 :
theorem Th105:
theorem Th106:
theorem
theorem Th108:
theorem Th109:
theorem
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem