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, x9, y, y9, x1, x19, y1, y19 being set st [[x,x9],[y,y9]] = [[x1,x19],[y1,y19]] holds
( x = x1 & y = y1 & x9 = x19 & y9 = y19 )
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 :
for f, g, b3 being Function holds
( b3 = f +* g iff ( dom b3 = (dom f) \/ (dom g) & ( for x being set st x in (dom f) \/ (dom g) holds
( ( x in dom g implies b3 . x = g . x ) & ( not x in dom g implies b3 . x = f . x ) ) ) ) );
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 :
for f, b2 being Function holds
( b2 = ~ f iff ( ( 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 ) ) );
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,
x9,
y9 being
set st
(
z = [[x,x9],[y,y9]] &
[x,y] in dom f &
[x9,y9] in dom g ) ) ) & ( for
x,
y,
x9,
y9 being
set st
[x,y] in dom f &
[x9,y9] in dom g holds
it . [x,x9],
[y,y9] = [(f . x,y),(g . x9,y9)] ) );
existence
ex b1 being Function st
( ( for z being set holds
( z in dom b1 iff ex x, y, x9, y9 being set st
( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) ) & ( for x, y, x9, y9 being set st [x,y] in dom f & [x9,y9] in dom g holds
b1 . [x,x9],[y,y9] = [(f . x,y),(g . x9,y9)] ) )
uniqueness
for b1, b2 being Function st ( for z being set holds
( z in dom b1 iff ex x, y, x9, y9 being set st
( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) ) & ( for x, y, x9, y9 being set st [x,y] in dom f & [x9,y9] in dom g holds
b1 . [x,x9],[y,y9] = [(f . x,y),(g . x9,y9)] ) & ( for z being set holds
( z in dom b2 iff ex x, y, x9, y9 being set st
( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) ) & ( for x, y, x9, y9 being set st [x,y] in dom f & [x9,y9] in dom g holds
b2 . [x,x9],[y,y9] = [(f . x,y),(g . x9,y9)] ) 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, x9, y9 being set st
( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) ) & ( for x, y, x9, y9 being set st [x,y] in dom f & [x9,y9] in dom g holds
b3 . [x,x9],[y,y9] = [(f . x,y),(g . x9,y9)] ) ) );
theorem Th57:
for
x,
x9,
y,
y9 being
set for
f,
g being
Function holds
(
[[x,x9],[y,y9]] in dom |:f,g:| iff (
[x,y] in dom f &
[x9,y9] in dom g ) )
theorem
for
x,
x9,
y,
y9 being
set for
f,
g being
Function st
[[x,x9],[y,y9]] in dom |:f,g:| holds
|:f,g:| . [x,x9],
[y,y9] = [(f . x,y),(g . x9,y9)]
theorem Th59:
theorem Th60:
for
X,
Y,
X9,
Y9 being
set for
f,
g being
Function st
dom f c= [:X,Y:] &
dom g c= [:X9,Y9:] holds
dom |:f,g:| c= [:[:X,X9:],[:Y,Y9:]:]
theorem Th61:
for
X,
Y,
X9,
Y9 being
set for
f,
g being
Function st
dom f = [:X,Y:] &
dom g = [:X9,Y9:] holds
dom |:f,g:| = [:[:X,X9:],[:Y,Y9:]:]
theorem
for
X,
Y,
Z,
X9,
Y9,
Z9 being
set for
f being
PartFunc of
[:X,Y:],
Z for
g being
PartFunc of
[:X9,Y9:],
Z9 holds
|:f,g:| is
PartFunc of
[:[:X,X9:],[:Y,Y9:]:],
[:Z,Z9:]
theorem Th63:
for
X,
Y,
Z,
X9,
Y9,
Z9 being
set for
f being
Function of
[:X,Y:],
Z for
g being
Function of
[:X9,Y9:],
Z9 st
Z <> {} &
Z9 <> {} holds
|:f,g:| is
Function of
[:[:X,X9:],[:Y,Y9:]:],
[:Z,Z9:]
theorem
for
X,
Y,
X9,
Y9 being
set for
D,
D9 being non
empty set for
f being
Function of
[:X,Y:],
D for
g being
Function of
[:X9,Y9:],
D9 holds
|:f,g:| is
Function of
[:[:X,X9:],[:Y,Y9:]:],
[:D,D9:] by Th63;
:: deftheorem defines --> FUNCT_4:def 4 :
for x, y, a, b being set holds x,y --> a,b = (x .--> a) +* (y .--> b);
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,
x9,
y9 being
set st
a <> b &
a,
b --> x,
y = a,
b --> x9,
y9 holds
(
x = x9 &
y = y9 )
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
canceled;
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th102:
theorem
theorem Th104:
begin
:: deftheorem defines +~ FUNCT_4:def 5 :
for f being Function
for x, y being set holds f +~ x,y = f +* ((x .--> y) * f);
theorem Th105:
theorem Th106:
theorem
theorem Th108:
theorem Th109:
theorem
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem