begin
theorem Th1:
theorem Th2:
Lm1:
now
let C,
D be non
empty set ;
for b being Element of D
for F being Function of [:C,D:],D ex g being Function of [:NAT,C:],D st
for a being Element of C holds
( g . (0,a) = b & ( for n being Element of NAT holds g . ((n + 1),a) = F . (a,(g . (n,a))) ) )let b be
Element of
D;
for F being Function of [:C,D:],D ex g being Function of [:NAT,C:],D st
for a being Element of C holds
( g . (0,a) = b & ( for n being Element of NAT holds g . ((n + 1),a) = F . (a,(g . (n,a))) ) )let F be
Function of
[:C,D:],
D;
ex g being Function of [:NAT,C:],D st
for a being Element of C holds
( g . (0,a) = b & ( for n being Element of NAT holds g . ((n + 1),a) = F . (a,(g . (n,a))) ) )thus
ex
g being
Function of
[:NAT,C:],
D st
for
a being
Element of
C holds
(
g . (
0,
a)
= b & ( for
n being
Element of
NAT holds
g . (
(n + 1),
a)
= F . (
a,
(g . (n,a))) ) )
verum
proof
A1:
for
a being
Element of
C ex
f being
Function of
NAT,
D st
(
f . 0 = b & ( for
n being
Element of
NAT holds
f . (n + 1) = F . (
a,
(f . n)) ) )
proof
let a be
Element of
C;
ex f being Function of NAT,D st
( f . 0 = b & ( for n being Element of NAT holds f . (n + 1) = F . (a,(f . n)) ) )
defpred S1[
Element of
NAT ,
Element of
D,
Element of
D]
means $3
= F . (
a,$2);
A2:
for
n being
Element of
NAT for
x being
Element of
D ex
y being
Element of
D st
S1[
n,
x,
y]
;
ex
f being
Function of
NAT,
D st
(
f . 0 = b & ( for
n being
Element of
NAT holds
S1[
n,
f . n,
f . (n + 1)] ) )
from RECDEF_1:sch 2(A2);
hence
ex
f being
Function of
NAT,
D st
(
f . 0 = b & ( for
n being
Element of
NAT holds
f . (n + 1) = F . (
a,
(f . n)) ) )
;
verum
end;
ex
g being
Function of
C,
(Funcs (NAT,D)) st
for
a being
Element of
C ex
f being
Function of
NAT,
D st
(
g . a = f &
f . 0 = b & ( for
n being
Element of
NAT holds
f . (n + 1) = F . (
a,
(f . n)) ) )
proof
set h =
{ [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being Function of NAT,D st
( f = l & f . 0 = b & ( for n being Element of NAT holds f . (n + 1) = F . (a,(f . n)) ) ) } ;
A3:
now
let x,
y1,
y2 be
set ;
( [x,y1] in { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being Function of NAT,D st
( f = l & f . 0 = b & ( for n being Element of NAT holds f . (n + 1) = F . (a,(f . n)) ) ) } & [x,y2] in { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being Function of NAT,D st
( f = l & f . 0 = b & ( for n being Element of NAT holds f . (n + 1) = F . (a,(f . n)) ) ) } implies y1 = y2 )assume that A4:
[x,y1] in { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being Function of NAT,D st
( f = l & f . 0 = b & ( for n being Element of NAT holds f . (n + 1) = F . (a,(f . n)) ) ) }
and A5:
[x,y2] in { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being Function of NAT,D st
( f = l & f . 0 = b & ( for n being Element of NAT holds f . (n + 1) = F . (a,(f . n)) ) ) }
;
y1 = y2consider a1 being
Element of
C,
l1 being
Element of
Funcs (
NAT,
D)
such that A6:
[x,y1] = [a1,l1]
and A7:
ex
f being
Function of
NAT,
D st
(
f = l1 &
f . 0 = b & ( for
n being
Element of
NAT holds
f . (n + 1) = F . (
a1,
(f . n)) ) )
by A4;
consider a2 being
Element of
C,
l2 being
Element of
Funcs (
NAT,
D)
such that A8:
[x,y2] = [a2,l2]
and A9:
ex
f being
Function of
NAT,
D st
(
f = l2 &
f . 0 = b & ( for
n being
Element of
NAT holds
f . (n + 1) = F . (
a2,
(f . n)) ) )
by A5;
consider f1 being
Function of
NAT,
D such that A10:
f1 = l1
and A11:
f1 . 0 = b
and A12:
for
n being
Element of
NAT holds
f1 . (n + 1) = F . (
a1,
(f1 . n))
by A7;
consider f2 being
Function of
NAT,
D such that A13:
f2 = l2
and A14:
f2 . 0 = b
and A15:
for
n being
Element of
NAT holds
f2 . (n + 1) = F . (
a2,
(f2 . n))
by A9;
A16:
a1 =
[x,y1] `1
by A6, MCART_1:def 1
.=
x
by MCART_1:def 1
.=
[a2,l2] `1
by A8, MCART_1:def 1
.=
a2
by MCART_1:def 1
;
A21:
(
NAT = dom f1 &
NAT = dom f2 )
by FUNCT_2:def 1;
thus y1 =
[a1,l1] `2
by A6, MCART_1:def 2
.=
l1
by MCART_1:def 2
.=
l2
by A10, A13, A21, A17, FUNCT_1:9
.=
[x,y2] `2
by A8, MCART_1:def 2
.=
y2
by MCART_1:def 2
;
verum
end;
now
let x be
set ;
( x in { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being Function of NAT,D st
( f = l & f . 0 = b & ( for n being Element of NAT holds f . (n + 1) = F . (a,(f . n)) ) ) } implies x in [:C,(Funcs (NAT,D)):] )assume
x in { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being Function of NAT,D st
( f = l & f . 0 = b & ( for n being Element of NAT holds f . (n + 1) = F . (a,(f . n)) ) ) }
;
x in [:C,(Funcs (NAT,D)):]then
ex
a being
Element of
C ex
l being
Element of
Funcs (
NAT,
D) st
(
x = [a,l] & ex
f being
Function of
NAT,
D st
(
f = l &
f . 0 = b & ( for
n being
Element of
NAT holds
f . (n + 1) = F . (
a,
(f . n)) ) ) )
;
hence
x in [:C,(Funcs (NAT,D)):]
by ZFMISC_1:def 2;
verum
end;
then reconsider h =
{ [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being Function of NAT,D st
( f = l & f . 0 = b & ( for n being Element of NAT holds f . (n + 1) = F . (a,(f . n)) ) ) } as
Relation of
C,
(Funcs (NAT,D)) by TARSKI:def 3;
A22:
for
x being
set st
x in C holds
x in dom h
for
x being
set st
x in dom h holds
x in C
;
then
dom h = C
by A22, TARSKI:2;
then reconsider h =
h as
Function of
C,
(Funcs (NAT,D)) by A3, FUNCT_1:def 1, FUNCT_2:def 1;
take
h
;
for a being Element of C ex f being Function of NAT,D st
( h . a = f & f . 0 = b & ( for n being Element of NAT holds f . (n + 1) = F . (a,(f . n)) ) )
for
a being
Element of
C ex
f being
Function of
NAT,
D st
(
h . a = f &
f . 0 = b & ( for
n being
Element of
NAT holds
f . (n + 1) = F . (
a,
(f . n)) ) )
proof
let a be
Element of
C;
ex f being Function of NAT,D st
( h . a = f & f . 0 = b & ( for n being Element of NAT holds f . (n + 1) = F . (a,(f . n)) ) )
dom h = C
by FUNCT_2:def 1;
then
[a,(h . a)] in h
by FUNCT_1:8;
then consider a9 being
Element of
C,
l being
Element of
Funcs (
NAT,
D)
such that A25:
[a,(h . a)] = [a9,l]
and A26:
ex
f9 being
Function of
NAT,
D st
(
f9 = l &
f9 . 0 = b & ( for
n being
Element of
NAT holds
f9 . (n + 1) = F . (
a9,
(f9 . n)) ) )
;
A27:
h . a =
[a9,l] `2
by A25, MCART_1:def 2
.=
l
by MCART_1:def 2
;
a =
[a9,l] `1
by A25, MCART_1:def 1
.=
a9
by MCART_1:def 1
;
hence
ex
f being
Function of
NAT,
D st
(
h . a = f &
f . 0 = b & ( for
n being
Element of
NAT holds
f . (n + 1) = F . (
a,
(f . n)) ) )
by A26, A27;
verum
end;
hence
for
a being
Element of
C ex
f being
Function of
NAT,
D st
(
h . a = f &
f . 0 = b & ( for
n being
Element of
NAT holds
f . (n + 1) = F . (
a,
(f . n)) ) )
;
verum
end;
then consider g being
Function of
C,
(Funcs (NAT,D)) such that A28:
for
a being
Element of
C ex
f being
Function of
NAT,
D st
(
g . a = f &
f . 0 = b & ( for
n being
Element of
NAT holds
f . (n + 1) = F . (
a,
(f . n)) ) )
;
set h =
{ [[n,a],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being Function of NAT,D st
( f = g . a & z = f . n ) } ;
A29:
now
let x,
y1,
y2 be
set ;
( [x,y1] in { [[n,a],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being Function of NAT,D st
( f = g . a & z = f . n ) } & [x,y2] in { [[n,a],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being Function of NAT,D st
( f = g . a & z = f . n ) } implies y1 = y2 )assume that A30:
[x,y1] in { [[n,a],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being Function of NAT,D st
( f = g . a & z = f . n ) }
and A31:
[x,y2] in { [[n,a],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being Function of NAT,D st
( f = g . a & z = f . n ) }
;
y1 = y2consider n1 being
Element of
NAT ,
a1 being
Element of
C,
z1 being
Element of
D such that A32:
[x,y1] = [[n1,a1],z1]
and A33:
ex
f1 being
Function of
NAT,
D st
(
f1 = g . a1 &
z1 = f1 . n1 )
by A30;
consider n2 being
Element of
NAT ,
a2 being
Element of
C,
z2 being
Element of
D such that A34:
[x,y2] = [[n2,a2],z2]
and A35:
ex
f2 being
Function of
NAT,
D st
(
f2 = g . a2 &
z2 = f2 . n2 )
by A31;
A36:
[n1,a1] =
[x,y1] `1
by A32, MCART_1:def 1
.=
x
by MCART_1:def 1
.=
[[n2,a2],z2] `1
by A34, MCART_1:def 1
.=
[n2,a2]
by MCART_1:def 1
;
then A37:
a1 =
[n2,a2] `2
by MCART_1:def 2
.=
a2
by MCART_1:def 2
;
n1 =
[n2,a2] `1
by A36, MCART_1:def 1
.=
n2
by MCART_1:def 1
;
hence y1 =
[x,y2] `2
by A32, A33, A34, A35, A37, MCART_1:def 2
.=
y2
by MCART_1:def 2
;
verum
end;
now
let x be
set ;
( x in { [[n,a],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being Function of NAT,D st
( f = g . a & z = f . n ) } implies x in [:[:NAT,C:],D:] )assume
x in { [[n,a],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being Function of NAT,D st
( f = g . a & z = f . n ) }
;
x in [:[:NAT,C:],D:]then consider n1 being
Element of
NAT ,
a1 being
Element of
C,
z1 being
Element of
D such that A38:
x = [[n1,a1],z1]
and
ex
f1 being
Function of
NAT,
D st
(
f1 = g . a1 &
z1 = f1 . n1 )
;
[n1,a1] in [:NAT,C:]
by ZFMISC_1:def 2;
hence
x in [:[:NAT,C:],D:]
by A38, ZFMISC_1:def 2;
verum
end;
then reconsider h =
{ [[n,a],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being Function of NAT,D st
( f = g . a & z = f . n ) } as
Relation of
[:NAT,C:],
D by TARSKI:def 3;
A39:
for
x being
set st
x in [:NAT,C:] holds
x in dom h
proof
let x be
set ;
( x in [:NAT,C:] implies x in dom h )
assume
x in [:NAT,C:]
;
x in dom h
then consider n,
d being
set such that A40:
n in NAT
and A41:
d in C
and A42:
x = [n,d]
by ZFMISC_1:def 2;
reconsider d =
d as
Element of
C by A41;
reconsider n =
n as
Element of
NAT by A40;
consider f9 being
Function of
NAT,
D such that A43:
g . d = f9
and
f9 . 0 = b
and
for
n being
Element of
NAT holds
f9 . (n + 1) = F . (
d,
(f9 . n))
by A28;
ex
z being
Element of
D ex
f being
Function of
NAT,
D st
(
f = g . d &
z = f . n )
proof
take
f9 . n
;
ex f being Function of NAT,D st
( f = g . d & f9 . n = f . n )
take
f9
;
( f9 = g . d & f9 . n = f9 . n )
thus
(
f9 = g . d &
f9 . n = f9 . n )
by A43;
verum
end;
then consider z being
Element of
D such that A44:
ex
f being
Function of
NAT,
D st
(
f = g . d &
z = f . n )
;
[x,z] in h
by A42, A44;
hence
x in dom h
by RELAT_1:def 4;
verum
end;
for
x being
set st
x in dom h holds
x in [:NAT,C:]
;
then
dom h = [:NAT,C:]
by A39, TARSKI:2;
then reconsider h =
h as
Function of
[:NAT,C:],
D by A29, FUNCT_1:def 1, FUNCT_2:def 1;
take
h
;
for a being Element of C holds
( h . (0,a) = b & ( for n being Element of NAT holds h . ((n + 1),a) = F . (a,(h . (n,a))) ) )
for
a being
Element of
C holds
(
h . (
0,
a)
= b & ( for
n being
Element of
NAT holds
h . (
(n + 1),
a)
= F . (
a,
(h . (n,a))) ) )
proof
let a be
Element of
C;
( h . (0,a) = b & ( for n being Element of NAT holds h . ((n + 1),a) = F . (a,(h . (n,a))) ) )
consider f9 being
Function of
NAT,
D such that A45:
g . a = f9
and A46:
f9 . 0 = b
and A47:
for
n being
Element of
NAT holds
f9 . (n + 1) = F . (
a,
(f9 . n))
by A28;
A48:
now
let k be
Element of
NAT ;
h . ((k + 1),a) = F . (a,(h . (k,a)))
[(k + 1),a] in [:NAT,C:]
by ZFMISC_1:def 2;
then
[(k + 1),a] in dom h
by FUNCT_2:def 1;
then consider u being
set such that A49:
[[(k + 1),a],u] in h
by RELAT_1:def 4;
[k,a] in [:NAT,C:]
by ZFMISC_1:def 2;
then
[k,a] in dom h
by FUNCT_2:def 1;
then consider v being
set such that A50:
[[k,a],v] in h
by RELAT_1:def 4;
consider n being
Element of
NAT ,
d being
Element of
C,
z being
Element of
D such that A51:
[[(k + 1),a],u] = [[n,d],z]
and A52:
ex
f1 being
Function of
NAT,
D st
(
f1 = g . d &
z = f1 . n )
by A49;
A53:
u =
[[n,d],z] `2
by A51, MCART_1:def 2
.=
z
by MCART_1:def 2
;
consider n1 being
Element of
NAT ,
d1 being
Element of
C,
z1 being
Element of
D such that A54:
[[k,a],v] = [[n1,d1],z1]
and A55:
ex
f2 being
Function of
NAT,
D st
(
f2 = g . d1 &
z1 = f2 . n1 )
by A50;
A56:
v =
[[n1,d1],z1] `2
by A54, MCART_1:def 2
.=
z1
by MCART_1:def 2
;
A57:
[(k + 1),a] =
[[n,d],z] `1
by A51, MCART_1:def 1
.=
[n,d]
by MCART_1:def 1
;
then A58:
d =
[(k + 1),a] `2
by MCART_1:def 2
.=
a
by MCART_1:def 2
;
A59:
[k,a] =
[[n1,d1],z1] `1
by A54, MCART_1:def 1
.=
[n1,d1]
by MCART_1:def 1
;
then A60:
n1 =
[k,a] `1
by MCART_1:def 1
.=
k
by MCART_1:def 1
;
A61:
d1 =
[k,a] `2
by A59, MCART_1:def 2
.=
a
by MCART_1:def 2
;
n =
[(k + 1),a] `1
by A57, MCART_1:def 1
.=
k + 1
by MCART_1:def 1
;
hence h . (
(k + 1),
a) =
f9 . (k + 1)
by A45, A49, A52, A53, A58, FUNCT_1:8
.=
F . (
a,
z1)
by A45, A47, A55, A60, A61
.=
F . (
a,
(h . (k,a)))
by A50, A56, FUNCT_1:8
;
verum
end;
[0,a] in [:NAT,C:]
by ZFMISC_1:def 2;
then
[0,a] in dom h
by FUNCT_2:def 1;
then consider u being
set such that A62:
[[0,a],u] in h
by RELAT_1:def 4;
consider n being
Element of
NAT ,
d being
Element of
C,
z being
Element of
D such that A63:
[[0,a],u] = [[n,d],z]
and A64:
ex
f1 being
Function of
NAT,
D st
(
f1 = g . d &
z = f1 . n )
by A62;
A65:
u =
[[n,d],z] `2
by A63, MCART_1:def 2
.=
z
by MCART_1:def 2
;
A66:
[0,a] =
[[n,d],z] `1
by A63, MCART_1:def 1
.=
[n,d]
by MCART_1:def 1
;
then A67:
d =
[0,a] `2
by MCART_1:def 2
.=
a
by MCART_1:def 2
;
n =
[0,a] `1
by A66, MCART_1:def 1
.=
0
by MCART_1:def 1
;
hence
(
h . (
0,
a)
= b & ( for
n being
Element of
NAT holds
h . (
(n + 1),
a)
= F . (
a,
(h . (n,a))) ) )
by A45, A46, A62, A64, A65, A67, A48, FUNCT_1:8;
verum
end;
hence
for
a being
Element of
C holds
(
h . (
0,
a)
= b & ( for
n being
Element of
NAT holds
h . (
(n + 1),
a)
= F . (
a,
(h . (n,a))) ) )
;
verum
end;
end;
Lm2:
now
let C,
D be non
empty set ;
for b being Element of D
for F being Function of [:D,C:],D ex g being Function of [:C,NAT:],D st
for a being Element of C holds
( g . (a,0) = b & ( for n being Element of NAT holds g . (a,(n + 1)) = F . ((g . (a,n)),a) ) )let b be
Element of
D;
for F being Function of [:D,C:],D ex g being Function of [:C,NAT:],D st
for a being Element of C holds
( g . (a,0) = b & ( for n being Element of NAT holds g . (a,(n + 1)) = F . ((g . (a,n)),a) ) )let F be
Function of
[:D,C:],
D;
ex g being Function of [:C,NAT:],D st
for a being Element of C holds
( g . (a,0) = b & ( for n being Element of NAT holds g . (a,(n + 1)) = F . ((g . (a,n)),a) ) )thus
ex
g being
Function of
[:C,NAT:],
D st
for
a being
Element of
C holds
(
g . (
a,
0)
= b & ( for
n being
Element of
NAT holds
g . (
a,
(n + 1))
= F . (
(g . (a,n)),
a) ) )
verum
proof
A1:
for
a being
Element of
C ex
f being
Function of
NAT,
D st
(
f . 0 = b & ( for
n being
Element of
NAT holds
f . (n + 1) = F . (
(f . n),
a) ) )
proof
let a be
Element of
C;
ex f being Function of NAT,D st
( f . 0 = b & ( for n being Element of NAT holds f . (n + 1) = F . ((f . n),a) ) )
defpred S1[
Element of
NAT ,
Element of
D,
Element of
D]
means $3
= F . ($2,
a);
A2:
for
n being
Element of
NAT for
x being
Element of
D ex
y being
Element of
D st
S1[
n,
x,
y]
;
ex
f being
Function of
NAT,
D st
(
f . 0 = b & ( for
n being
Element of
NAT holds
S1[
n,
f . n,
f . (n + 1)] ) )
from RECDEF_1:sch 2(A2);
hence
ex
f being
Function of
NAT,
D st
(
f . 0 = b & ( for
n being
Element of
NAT holds
f . (n + 1) = F . (
(f . n),
a) ) )
;
verum
end;
ex
g being
Function of
C,
(Funcs (NAT,D)) st
for
a being
Element of
C ex
f being
Function of
NAT,
D st
(
g . a = f &
f . 0 = b & ( for
n being
Element of
NAT holds
f . (n + 1) = F . (
(f . n),
a) ) )
proof
set h =
{ [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being Function of NAT,D st
( f = l & f . 0 = b & ( for n being Element of NAT holds f . (n + 1) = F . ((f . n),a) ) ) } ;
A3:
now
let x,
y1,
y2 be
set ;
( [x,y1] in { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being Function of NAT,D st
( f = l & f . 0 = b & ( for n being Element of NAT holds f . (n + 1) = F . ((f . n),a) ) ) } & [x,y2] in { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being Function of NAT,D st
( f = l & f . 0 = b & ( for n being Element of NAT holds f . (n + 1) = F . ((f . n),a) ) ) } implies y1 = y2 )assume that A4:
[x,y1] in { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being Function of NAT,D st
( f = l & f . 0 = b & ( for n being Element of NAT holds f . (n + 1) = F . ((f . n),a) ) ) }
and A5:
[x,y2] in { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being Function of NAT,D st
( f = l & f . 0 = b & ( for n being Element of NAT holds f . (n + 1) = F . ((f . n),a) ) ) }
;
y1 = y2consider a1 being
Element of
C,
l1 being
Element of
Funcs (
NAT,
D)
such that A6:
[x,y1] = [a1,l1]
and A7:
ex
f being
Function of
NAT,
D st
(
f = l1 &
f . 0 = b & ( for
n being
Element of
NAT holds
f . (n + 1) = F . (
(f . n),
a1) ) )
by A4;
consider a2 being
Element of
C,
l2 being
Element of
Funcs (
NAT,
D)
such that A8:
[x,y2] = [a2,l2]
and A9:
ex
f being
Function of
NAT,
D st
(
f = l2 &
f . 0 = b & ( for
n being
Element of
NAT holds
f . (n + 1) = F . (
(f . n),
a2) ) )
by A5;
consider f1 being
Function of
NAT,
D such that A10:
f1 = l1
and A11:
f1 . 0 = b
and A12:
for
n being
Element of
NAT holds
f1 . (n + 1) = F . (
(f1 . n),
a1)
by A7;
consider f2 being
Function of
NAT,
D such that A13:
f2 = l2
and A14:
f2 . 0 = b
and A15:
for
n being
Element of
NAT holds
f2 . (n + 1) = F . (
(f2 . n),
a2)
by A9;
A16:
a1 =
[x,y1] `1
by A6, MCART_1:def 1
.=
x
by MCART_1:def 1
.=
[a2,l2] `1
by A8, MCART_1:def 1
.=
a2
by MCART_1:def 1
;
A21:
(
NAT = dom f1 &
NAT = dom f2 )
by FUNCT_2:def 1;
thus y1 =
[a1,l1] `2
by A6, MCART_1:def 2
.=
l1
by MCART_1:def 2
.=
l2
by A10, A13, A21, A17, FUNCT_1:9
.=
[x,y2] `2
by A8, MCART_1:def 2
.=
y2
by MCART_1:def 2
;
verum
end;
now
let x be
set ;
( x in { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being Function of NAT,D st
( f = l & f . 0 = b & ( for n being Element of NAT holds f . (n + 1) = F . ((f . n),a) ) ) } implies x in [:C,(Funcs (NAT,D)):] )assume
x in { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being Function of NAT,D st
( f = l & f . 0 = b & ( for n being Element of NAT holds f . (n + 1) = F . ((f . n),a) ) ) }
;
x in [:C,(Funcs (NAT,D)):]then
ex
a being
Element of
C ex
l being
Element of
Funcs (
NAT,
D) st
(
x = [a,l] & ex
f being
Function of
NAT,
D st
(
f = l &
f . 0 = b & ( for
n being
Element of
NAT holds
f . (n + 1) = F . (
(f . n),
a) ) ) )
;
hence
x in [:C,(Funcs (NAT,D)):]
by ZFMISC_1:def 2;
verum
end;
then reconsider h =
{ [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being Function of NAT,D st
( f = l & f . 0 = b & ( for n being Element of NAT holds f . (n + 1) = F . ((f . n),a) ) ) } as
Relation of
C,
(Funcs (NAT,D)) by TARSKI:def 3;
A22:
for
x being
set st
x in C holds
x in dom h
for
x being
set st
x in dom h holds
x in C
;
then
dom h = C
by A22, TARSKI:2;
then reconsider h =
h as
Function of
C,
(Funcs (NAT,D)) by A3, FUNCT_1:def 1, FUNCT_2:def 1;
take
h
;
for a being Element of C ex f being Function of NAT,D st
( h . a = f & f . 0 = b & ( for n being Element of NAT holds f . (n + 1) = F . ((f . n),a) ) )
for
a being
Element of
C ex
f being
Function of
NAT,
D st
(
h . a = f &
f . 0 = b & ( for
n being
Element of
NAT holds
f . (n + 1) = F . (
(f . n),
a) ) )
proof
let a be
Element of
C;
ex f being Function of NAT,D st
( h . a = f & f . 0 = b & ( for n being Element of NAT holds f . (n + 1) = F . ((f . n),a) ) )
dom h = C
by FUNCT_2:def 1;
then
[a,(h . a)] in h
by FUNCT_1:8;
then consider a9 being
Element of
C,
l being
Element of
Funcs (
NAT,
D)
such that A25:
[a,(h . a)] = [a9,l]
and A26:
ex
f9 being
Function of
NAT,
D st
(
f9 = l &
f9 . 0 = b & ( for
n being
Element of
NAT holds
f9 . (n + 1) = F . (
(f9 . n),
a9) ) )
;
A27:
h . a =
[a9,l] `2
by A25, MCART_1:def 2
.=
l
by MCART_1:def 2
;
a =
[a9,l] `1
by A25, MCART_1:def 1
.=
a9
by MCART_1:def 1
;
hence
ex
f being
Function of
NAT,
D st
(
h . a = f &
f . 0 = b & ( for
n being
Element of
NAT holds
f . (n + 1) = F . (
(f . n),
a) ) )
by A26, A27;
verum
end;
hence
for
a being
Element of
C ex
f being
Function of
NAT,
D st
(
h . a = f &
f . 0 = b & ( for
n being
Element of
NAT holds
f . (n + 1) = F . (
(f . n),
a) ) )
;
verum
end;
then consider g being
Function of
C,
(Funcs (NAT,D)) such that A28:
for
a being
Element of
C ex
f being
Function of
NAT,
D st
(
g . a = f &
f . 0 = b & ( for
n being
Element of
NAT holds
f . (n + 1) = F . (
(f . n),
a) ) )
;
set h =
{ [[a,n],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being Function of NAT,D st
( f = g . a & z = f . n ) } ;
A29:
now
let x,
y1,
y2 be
set ;
( [x,y1] in { [[a,n],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being Function of NAT,D st
( f = g . a & z = f . n ) } & [x,y2] in { [[a,n],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being Function of NAT,D st
( f = g . a & z = f . n ) } implies y1 = y2 )assume that A30:
[x,y1] in { [[a,n],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being Function of NAT,D st
( f = g . a & z = f . n ) }
and A31:
[x,y2] in { [[a,n],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being Function of NAT,D st
( f = g . a & z = f . n ) }
;
y1 = y2consider n1 being
Element of
NAT ,
a1 being
Element of
C,
z1 being
Element of
D such that A32:
[x,y1] = [[a1,n1],z1]
and A33:
ex
f1 being
Function of
NAT,
D st
(
f1 = g . a1 &
z1 = f1 . n1 )
by A30;
consider n2 being
Element of
NAT ,
a2 being
Element of
C,
z2 being
Element of
D such that A34:
[x,y2] = [[a2,n2],z2]
and A35:
ex
f2 being
Function of
NAT,
D st
(
f2 = g . a2 &
z2 = f2 . n2 )
by A31;
A36:
[a1,n1] =
[x,y1] `1
by A32, MCART_1:def 1
.=
x
by MCART_1:def 1
.=
[[a2,n2],z2] `1
by A34, MCART_1:def 1
.=
[a2,n2]
by MCART_1:def 1
;
then A37:
n1 =
[a2,n2] `2
by MCART_1:def 2
.=
n2
by MCART_1:def 2
;
a1 =
[a2,n2] `1
by A36, MCART_1:def 1
.=
a2
by MCART_1:def 1
;
hence y1 =
[x,y2] `2
by A32, A33, A34, A35, A37, MCART_1:def 2
.=
y2
by MCART_1:def 2
;
verum
end;
now
let x be
set ;
( x in { [[a,n],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being Function of NAT,D st
( f = g . a & z = f . n ) } implies x in [:[:C,NAT:],D:] )assume
x in { [[a,n],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being Function of NAT,D st
( f = g . a & z = f . n ) }
;
x in [:[:C,NAT:],D:]then consider n1 being
Element of
NAT ,
a1 being
Element of
C,
z1 being
Element of
D such that A38:
x = [[a1,n1],z1]
and
ex
f1 being
Function of
NAT,
D st
(
f1 = g . a1 &
z1 = f1 . n1 )
;
[a1,n1] in [:C,NAT:]
by ZFMISC_1:def 2;
hence
x in [:[:C,NAT:],D:]
by A38, ZFMISC_1:def 2;
verum
end;
then reconsider h =
{ [[a,n],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being Function of NAT,D st
( f = g . a & z = f . n ) } as
Relation of
[:C,NAT:],
D by TARSKI:def 3;
A39:
for
x being
set st
x in [:C,NAT:] holds
x in dom h
proof
let x be
set ;
( x in [:C,NAT:] implies x in dom h )
assume
x in [:C,NAT:]
;
x in dom h
then consider d,
n being
set such that A40:
d in C
and A41:
n in NAT
and A42:
x = [d,n]
by ZFMISC_1:def 2;
reconsider d =
d as
Element of
C by A40;
reconsider n =
n as
Element of
NAT by A41;
consider f9 being
Function of
NAT,
D such that A43:
g . d = f9
and
f9 . 0 = b
and
for
n being
Element of
NAT holds
f9 . (n + 1) = F . (
(f9 . n),
d)
by A28;
ex
z being
Element of
D ex
f being
Function of
NAT,
D st
(
f = g . d &
z = f . n )
proof
take
f9 . n
;
ex f being Function of NAT,D st
( f = g . d & f9 . n = f . n )
take
f9
;
( f9 = g . d & f9 . n = f9 . n )
thus
(
f9 = g . d &
f9 . n = f9 . n )
by A43;
verum
end;
then consider z being
Element of
D such that A44:
ex
f being
Function of
NAT,
D st
(
f = g . d &
z = f . n )
;
[x,z] in h
by A42, A44;
hence
x in dom h
by RELAT_1:def 4;
verum
end;
for
x being
set st
x in dom h holds
x in [:C,NAT:]
;
then
dom h = [:C,NAT:]
by A39, TARSKI:2;
then reconsider h =
h as
Function of
[:C,NAT:],
D by A29, FUNCT_1:def 1, FUNCT_2:def 1;
take
h
;
for a being Element of C holds
( h . (a,0) = b & ( for n being Element of NAT holds h . (a,(n + 1)) = F . ((h . (a,n)),a) ) )
for
a being
Element of
C holds
(
h . (
a,
0)
= b & ( for
n being
Element of
NAT holds
h . (
a,
(n + 1))
= F . (
(h . (a,n)),
a) ) )
proof
let a be
Element of
C;
( h . (a,0) = b & ( for n being Element of NAT holds h . (a,(n + 1)) = F . ((h . (a,n)),a) ) )
consider f9 being
Function of
NAT,
D such that A45:
g . a = f9
and A46:
f9 . 0 = b
and A47:
for
n being
Element of
NAT holds
f9 . (n + 1) = F . (
(f9 . n),
a)
by A28;
A48:
now
let k be
Element of
NAT ;
h . (a,(k + 1)) = F . ((h . (a,k)),a)
[a,(k + 1)] in [:C,NAT:]
by ZFMISC_1:def 2;
then
[a,(k + 1)] in dom h
by FUNCT_2:def 1;
then consider u being
set such that A49:
[[a,(k + 1)],u] in h
by RELAT_1:def 4;
[a,k] in [:C,NAT:]
by ZFMISC_1:def 2;
then
[a,k] in dom h
by FUNCT_2:def 1;
then consider v being
set such that A50:
[[a,k],v] in h
by RELAT_1:def 4;
consider n1 being
Element of
NAT ,
d1 being
Element of
C,
z1 being
Element of
D such that A51:
[[a,k],v] = [[d1,n1],z1]
and A52:
ex
f2 being
Function of
NAT,
D st
(
f2 = g . d1 &
z1 = f2 . n1 )
by A50;
A53:
v =
[[d1,n1],z1] `2
by A51, MCART_1:def 2
.=
z1
by MCART_1:def 2
;
A54:
[a,k] =
[[d1,n1],z1] `1
by A51, MCART_1:def 1
.=
[d1,n1]
by MCART_1:def 1
;
then A55:
n1 =
[a,k] `2
by MCART_1:def 2
.=
k
by MCART_1:def 2
;
consider f2 being
Function of
NAT,
D such that A56:
f2 = g . d1
and A57:
z1 = f2 . n1
by A52;
consider n being
Element of
NAT ,
d being
Element of
C,
z being
Element of
D such that A58:
[[a,(k + 1)],u] = [[d,n],z]
and A59:
ex
f1 being
Function of
NAT,
D st
(
f1 = g . d &
z = f1 . n )
by A49;
A60:
[a,(k + 1)] =
[[d,n],z] `1
by A58, MCART_1:def 1
.=
[d,n]
by MCART_1:def 1
;
then A61:
n =
[a,(k + 1)] `2
by MCART_1:def 2
.=
k + 1
by MCART_1:def 2
;
A62:
d1 =
[a,k] `1
by A54, MCART_1:def 1
.=
a
by MCART_1:def 1
;
A63:
d =
[a,(k + 1)] `1
by A60, MCART_1:def 1
.=
a
by MCART_1:def 1
;
u =
[[d,n],z] `2
by A58, MCART_1:def 2
.=
z
by MCART_1:def 2
;
hence h . (
a,
(k + 1)) =
f9 . n
by A45, A49, A59, A63, FUNCT_1:8
.=
F . (
(f2 . n1),
a)
by A45, A47, A61, A56, A55, A62
.=
F . (
(h . (a,k)),
a)
by A50, A57, A53, FUNCT_1:8
;
verum
end;
[a,0] in [:C,NAT:]
by ZFMISC_1:def 2;
then
[a,0] in dom h
by FUNCT_2:def 1;
then consider u being
set such that A64:
[[a,0],u] in h
by RELAT_1:def 4;
consider n being
Element of
NAT ,
d being
Element of
C,
z being
Element of
D such that A65:
[[a,0],u] = [[d,n],z]
and A66:
ex
f1 being
Function of
NAT,
D st
(
f1 = g . d &
z = f1 . n )
by A64;
A67:
u =
[[d,n],z] `2
by A65, MCART_1:def 2
.=
z
by MCART_1:def 2
;
A68:
[a,0] =
[[d,n],z] `1
by A65, MCART_1:def 1
.=
[d,n]
by MCART_1:def 1
;
then A69:
d =
[a,0] `1
by MCART_1:def 1
.=
a
by MCART_1:def 1
;
n =
[a,0] `2
by A68, MCART_1:def 2
.=
0
by MCART_1:def 2
;
hence
(
h . (
a,
0)
= b & ( for
n being
Element of
NAT holds
h . (
a,
(n + 1))
= F . (
(h . (a,n)),
a) ) )
by A45, A46, A64, A66, A67, A69, A48, FUNCT_1:8;
verum
end;
hence
for
a being
Element of
C holds
(
h . (
a,
0)
= b & ( for
n being
Element of
NAT holds
h . (
a,
(n + 1))
= F . (
(h . (a,n)),
a) ) )
;
verum
end;
end;
begin
theorem Th3:
theorem
theorem Th5:
theorem
:: deftheorem BINOM:def 1 :
canceled;
:: deftheorem BINOM:def 2 :
canceled;
:: deftheorem BINOM:def 3 :
canceled;
:: deftheorem Def4 defines + BINOM:def 4 :
for R being non empty addLoopStr
for p, q, b4 being FinSequence of the carrier of R holds
( b4 = p + q iff ( dom b4 = dom p & ( for i being Nat st 1 <= i & i <= len b4 holds
b4 /. i = (p /. i) + (q /. i) ) ) );
theorem Th7:
begin
:: deftheorem defines |^ BINOM:def 5 :
for R being non empty unital multMagma
for a being Element of R
for n being Nat holds a |^ n = (power R) . (a,n);
theorem Th8:
theorem
canceled;
theorem
theorem Th11:
theorem
begin
definition
let R be non
empty addLoopStr ;
func Nat-mult-left R -> Function of
[:NAT, the carrier of R:], the
carrier of
R means :
Def6:
for
a being
Element of
R holds
(
it . (
0,
a)
= 0. R & ( for
n being
Element of
NAT holds
it . (
(n + 1),
a)
= a + (it . (n,a)) ) );
existence
ex b1 being Function of [:NAT, the carrier of R:], the carrier of R st
for a being Element of R holds
( b1 . (0,a) = 0. R & ( for n being Element of NAT holds b1 . ((n + 1),a) = a + (b1 . (n,a)) ) )
uniqueness
for b1, b2 being Function of [:NAT, the carrier of R:], the carrier of R st ( for a being Element of R holds
( b1 . (0,a) = 0. R & ( for n being Element of NAT holds b1 . ((n + 1),a) = a + (b1 . (n,a)) ) ) ) & ( for a being Element of R holds
( b2 . (0,a) = 0. R & ( for n being Element of NAT holds b2 . ((n + 1),a) = a + (b2 . (n,a)) ) ) ) holds
b1 = b2
func Nat-mult-right R -> Function of
[: the carrier of R,NAT:], the
carrier of
R means :
Def7:
for
a being
Element of
R holds
(
it . (
a,
0)
= 0. R & ( for
n being
Element of
NAT holds
it . (
a,
(n + 1))
= (it . (a,n)) + a ) );
existence
ex b1 being Function of [: the carrier of R,NAT:], the carrier of R st
for a being Element of R holds
( b1 . (a,0) = 0. R & ( for n being Element of NAT holds b1 . (a,(n + 1)) = (b1 . (a,n)) + a ) )
uniqueness
for b1, b2 being Function of [: the carrier of R,NAT:], the carrier of R st ( for a being Element of R holds
( b1 . (a,0) = 0. R & ( for n being Element of NAT holds b1 . (a,(n + 1)) = (b1 . (a,n)) + a ) ) ) & ( for a being Element of R holds
( b2 . (a,0) = 0. R & ( for n being Element of NAT holds b2 . (a,(n + 1)) = (b2 . (a,n)) + a ) ) ) holds
b1 = b2
end;
:: deftheorem Def6 defines Nat-mult-left BINOM:def 6 :
for R being non empty addLoopStr
for b2 being Function of [:NAT, the carrier of R:], the carrier of R holds
( b2 = Nat-mult-left R iff for a being Element of R holds
( b2 . (0,a) = 0. R & ( for n being Element of NAT holds b2 . ((n + 1),a) = a + (b2 . (n,a)) ) ) );
:: deftheorem Def7 defines Nat-mult-right BINOM:def 7 :
for R being non empty addLoopStr
for b2 being Function of [: the carrier of R,NAT:], the carrier of R holds
( b2 = Nat-mult-right R iff for a being Element of R holds
( b2 . (a,0) = 0. R & ( for n being Element of NAT holds b2 . (a,(n + 1)) = (b2 . (a,n)) + a ) ) );
:: deftheorem defines * BINOM:def 8 :
for R being non empty addLoopStr
for a being Element of R
for n being Element of NAT holds n * a = (Nat-mult-left R) . (n,a);
:: deftheorem defines * BINOM:def 9 :
for R being non empty addLoopStr
for a being Element of R
for n being Element of NAT holds a * n = (Nat-mult-right R) . (a,n);
theorem
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem
theorem Th20:
theorem Th21:
theorem Th22:
begin
definition
let R be non
empty unital doubleLoopStr ;
let a,
b be
Element of
R;
let n be
Element of
NAT ;
func (
a,
b)
In_Power n -> FinSequence of the
carrier of
R means :
Def10:
(
len it = n + 1 & ( for
i,
l,
m being
Element of
NAT st
i in dom it &
m = i - 1 &
l = n - m holds
it /. i = ((n choose m) * (a |^ l)) * (b |^ m) ) );
existence
ex b1 being FinSequence of the carrier of R st
( len b1 = n + 1 & ( for i, l, m being Element of NAT st i in dom b1 & m = i - 1 & l = n - m holds
b1 /. i = ((n choose m) * (a |^ l)) * (b |^ m) ) )
uniqueness
for b1, b2 being FinSequence of the carrier of R st len b1 = n + 1 & ( for i, l, m being Element of NAT st i in dom b1 & m = i - 1 & l = n - m holds
b1 /. i = ((n choose m) * (a |^ l)) * (b |^ m) ) & len b2 = n + 1 & ( for i, l, m being Element of NAT st i in dom b2 & m = i - 1 & l = n - m holds
b2 /. i = ((n choose m) * (a |^ l)) * (b |^ m) ) holds
b1 = b2
end;
:: deftheorem Def10 defines In_Power BINOM:def 10 :
for R being non empty unital doubleLoopStr
for a, b being Element of R
for n being Element of NAT
for b5 being FinSequence of the carrier of R holds
( b5 = (a,b) In_Power n iff ( len b5 = n + 1 & ( for i, l, m being Element of NAT st i in dom b5 & m = i - 1 & l = n - m holds
b5 /. i = ((n choose m) * (a |^ l)) * (b |^ m) ) ) );
theorem Th23:
theorem Th24:
theorem Th25:
theorem
theorem
theorem