begin
Lm1:
now for C, D being 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 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 for x, y1, y2 being set st [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)) ) ) } holds
y1 = y2
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 =
[a1,l1] `1
.=
[x,y1] `1
by A6
.=
x
.=
[x,y2] `1
.=
[a2,l2] `1
by A8
.=
a2
;
A21:
(
NAT = dom f1 &
NAT = dom f2 )
by FUNCT_2:def 1;
thus y1 =
[x,y1] `2
.=
[a1,l1] `2
by A6
.=
l1
.=
l2
by A10, A13, A21, A17, FUNCT_1:2
.=
[a2,l2] `2
.=
[x,y2] `2
by A8
.=
y2
;
verum
end;
now for x being set st 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)) ) ) } holds
x in [:C,(Funcs (NAT,D)):]
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:1;
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:1;
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 =
[a,(h . a)] `2
.=
[a9,l] `2
by A25
.=
l
;
a =
[a,(h . a)] `1
.=
[a9,l] `1
by A25
.=
a9
;
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 for x, y1, y2 being set st [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 ) } holds
y1 = y2
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] =
[[n1,a1],z1] `1
.=
[x,y1] `1
by A32
.=
x
.=
[x,y2] `1
.=
[[n2,a2],z2] `1
by A34
.=
[n2,a2]
;
A37:
a1 =
[n1,a1] `2
.=
[n2,a2] `2
by A36
.=
a2
;
A38:
n1 =
[n1,a1] `1
.=
[n2,a2] `1
by A36
.=
n2
;
thus y1 =
[x,y1] `2
.=
[x,y2] `2
by A32, A33, A34, A35, A37, A38
.=
y2
;
verum
end;
now for x being set st 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 ) } holds
x in [:[:NAT,C:],D:]
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 A39:
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 A39, 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;
A40:
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 A41:
n in NAT
and A42:
d in C
and A43:
x = [n,d]
by ZFMISC_1:def 2;
reconsider d =
d as
Element of
C by A42;
reconsider n =
n as
Element of
NAT by A41;
consider f9 being
Function of
NAT,
D such that A44:
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 A44;
verum
end;
then consider z being
Element of
D such that A45:
ex
f being
Function of
NAT,
D st
(
f = g . d &
z = f . n )
;
[x,z] in h
by A43, A45;
hence
x in dom h
by XTUPLE_0:def 12;
verum
end;
for
x being
set st
x in dom h holds
x in [:NAT,C:]
;
then
dom h = [:NAT,C:]
by A40, TARSKI:1;
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 A46:
g . a = f9
and A47:
f9 . 0 = b
and A48:
for
n being
Element of
NAT holds
f9 . (n + 1) = F . (
a,
(f9 . n))
by A28;
A49:
now for k being Element of NAT holds h . ((k + 1),a) = F . (a,(h . (k,a)))
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 A50:
[[(k + 1),a],u] in h
by XTUPLE_0:def 12;
[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 A51:
[[k,a],v] in h
by XTUPLE_0:def 12;
consider n being
Element of
NAT ,
d being
Element of
C,
z being
Element of
D such that A52:
[[(k + 1),a],u] = [[n,d],z]
and A53:
ex
f1 being
Function of
NAT,
D st
(
f1 = g . d &
z = f1 . n )
by A50;
A54:
u =
[[(k + 1),a],u] `2
.=
[[n,d],z] `2
by A52
.=
z
;
consider n1 being
Element of
NAT ,
d1 being
Element of
C,
z1 being
Element of
D such that A55:
[[k,a],v] = [[n1,d1],z1]
and A56:
ex
f2 being
Function of
NAT,
D st
(
f2 = g . d1 &
z1 = f2 . n1 )
by A51;
A57:
v =
[[k,a],v] `2
.=
[[n1,d1],z1] `2
by A55
.=
z1
;
A58:
[(k + 1),a] =
[[(k + 1),a],u] `1
.=
[[n,d],z] `1
by A52
.=
[n,d]
;
A59:
d =
[n,d] `2
.=
[(k + 1),a] `2
by A58
.=
a
;
A60:
[k,a] =
[[k,a],v] `1
.=
[[n1,d1],z1] `1
by A55
.=
[n1,d1]
;
A61:
n1 =
[n1,d1] `1
.=
[k,a] `1
by A60
.=
k
;
A62:
d1 =
[n1,d1] `2
.=
[k,a] `2
by A60
.=
a
;
n =
[n,d] `1
.=
[(k + 1),a] `1
by A58
.=
k + 1
;
hence h . (
(k + 1),
a) =
f9 . (k + 1)
by A46, A50, A53, A54, A59, FUNCT_1:1
.=
F . (
a,
z1)
by A46, A48, A56, A61, A62
.=
F . (
a,
(h . (k,a)))
by A51, A57, FUNCT_1:1
;
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 A63:
[[0,a],u] in h
by XTUPLE_0:def 12;
consider n being
Element of
NAT ,
d being
Element of
C,
z being
Element of
D such that A64:
[[0,a],u] = [[n,d],z]
and A65:
ex
f1 being
Function of
NAT,
D st
(
f1 = g . d &
z = f1 . n )
by A63;
A66:
u =
[[0,a],u] `2
.=
[[n,d],z] `2
by A64
.=
z
;
A67:
[0,a] =
[[0,a],u] `1
.=
[[n,d],z] `1
by A64
.=
[n,d]
;
A68:
d =
[n,d] `2
.=
[0,a] `2
by A67
.=
a
;
n =
[n,d] `1
.=
[0,a] `1
by A67
.=
0
;
hence
(
h . (
0,
a)
= b & ( for
n being
Element of
NAT holds
h . (
(n + 1),
a)
= F . (
a,
(h . (n,a))) ) )
by A46, A47, A63, A65, A66, A68, A49, FUNCT_1:1;
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 for C, D being 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 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 for x, y1, y2 being set st [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) ) ) } holds
y1 = y2
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 =
[a1,l1] `1
.=
[x,y1] `1
by A6
.=
x
.=
[x,y2] `1
.=
[a2,l2] `1
by A8
.=
a2
;
A21:
(
NAT = dom f1 &
NAT = dom f2 )
by FUNCT_2:def 1;
thus y1 =
[x,y1] `2
.=
[a1,l1] `2
by A6
.=
l1
.=
l2
by A10, A13, A21, A17, FUNCT_1:2
.=
[a2,l2] `2
.=
[x,y2] `2
by A8
.=
y2
;
verum
end;
now for x being set st 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) ) ) } holds
x in [:C,(Funcs (NAT,D)):]
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:1;
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:1;
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 =
[a,(h . a)] `2
.=
[a9,l] `2
by A25
.=
l
;
a =
[a,(h . a)] `1
.=
[a9,l] `1
by A25
.=
a9
;
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 for x, y1, y2 being set st [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 ) } holds
y1 = y2
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] =
[[a1,n1],z1] `1
.=
[x,y1] `1
by A32
.=
x
.=
[x,y2] `1
.=
[[a2,n2],z2] `1
by A34
.=
[a2,n2]
;
A37:
n1 =
[a1,n1] `2
.=
[a2,n2] `2
by A36
.=
n2
;
A38:
a1 =
[a1,n1] `1
.=
[a2,n2] `1
by A36
.=
a2
;
thus y1 =
[x,y1] `2
.=
[x,y2] `2
by A32, A33, A34, A35, A37, A38
.=
y2
;
verum
end;
now for x being set st 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 ) } holds
x in [:[:C,NAT:],D:]
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 A39:
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 A39, 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;
A40:
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 A41:
d in C
and A42:
n in NAT
and A43:
x = [d,n]
by ZFMISC_1:def 2;
reconsider d =
d as
Element of
C by A41;
reconsider n =
n as
Element of
NAT by A42;
consider f9 being
Function of
NAT,
D such that A44:
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 A44;
verum
end;
then consider z being
Element of
D such that A45:
ex
f being
Function of
NAT,
D st
(
f = g . d &
z = f . n )
;
[x,z] in h
by A43, A45;
hence
x in dom h
by XTUPLE_0:def 12;
verum
end;
for
x being
set st
x in dom h holds
x in [:C,NAT:]
;
then
dom h = [:C,NAT:]
by A40, TARSKI:1;
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 A46:
g . a = f9
and A47:
f9 . 0 = b
and A48:
for
n being
Element of
NAT holds
f9 . (n + 1) = F . (
(f9 . n),
a)
by A28;
A49:
now for k being Element of NAT holds h . (a,(k + 1)) = F . ((h . (a,k)),a)
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 A50:
[[a,(k + 1)],u] in h
by XTUPLE_0:def 12;
[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 A51:
[[a,k],v] in h
by XTUPLE_0:def 12;
consider n1 being
Element of
NAT ,
d1 being
Element of
C,
z1 being
Element of
D such that A52:
[[a,k],v] = [[d1,n1],z1]
and A53:
ex
f2 being
Function of
NAT,
D st
(
f2 = g . d1 &
z1 = f2 . n1 )
by A51;
A54:
v =
[[a,k],v] `2
.=
[[d1,n1],z1] `2
by A52
.=
z1
;
A55:
[a,k] =
[[a,k],v] `1
.=
[[d1,n1],z1] `1
by A52
.=
[d1,n1]
;
A56:
n1 =
[d1,n1] `2
.=
[a,k] `2
by A55
.=
k
;
consider f2 being
Function of
NAT,
D such that A57:
f2 = g . d1
and A58:
z1 = f2 . n1
by A53;
consider n being
Element of
NAT ,
d being
Element of
C,
z being
Element of
D such that A59:
[[a,(k + 1)],u] = [[d,n],z]
and A60:
ex
f1 being
Function of
NAT,
D st
(
f1 = g . d &
z = f1 . n )
by A50;
A61:
[a,(k + 1)] =
[[a,(k + 1)],u] `1
.=
[[d,n],z] `1
by A59
.=
[d,n]
;
A62:
n =
[d,n] `2
.=
[a,(k + 1)] `2
by A61
.=
k + 1
;
A63:
d1 =
[d1,n1] `1
.=
[a,k] `1
by A55
.=
a
;
A64:
d =
[d,n] `1
.=
[a,(k + 1)] `1
by A61
.=
a
;
u =
[[a,(k + 1)],u] `2
.=
[[d,n],z] `2
by A59
.=
z
;
hence h . (
a,
(k + 1)) =
f9 . n
by A46, A50, A60, A64, FUNCT_1:1
.=
F . (
(f2 . n1),
a)
by A46, A48, A62, A57, A56, A63
.=
F . (
(h . (a,k)),
a)
by A51, A58, A54, FUNCT_1:1
;
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 A65:
[[a,0],u] in h
by XTUPLE_0:def 12;
consider n being
Element of
NAT ,
d being
Element of
C,
z being
Element of
D such that A66:
[[a,0],u] = [[d,n],z]
and A67:
ex
f1 being
Function of
NAT,
D st
(
f1 = g . d &
z = f1 . n )
by A65;
A68:
u =
[[a,0],u] `2
.=
[[d,n],z] `2
by A66
.=
z
;
A69:
[a,0] =
[[a,0],u] `1
.=
[[d,n],z] `1
by A66
.=
[d,n]
;
A70:
d =
[d,n] `1
.=
[a,0] `1
by A69
.=
a
;
n =
[d,n] `2
.=
[a,0] `2
by A69
.=
0
;
hence
(
h . (
a,
0)
= b & ( for
n being
Element of
NAT holds
h . (
a,
(n + 1))
= F . (
(h . (a,n)),
a) ) )
by A46, A47, A65, A67, A68, A70, A49, FUNCT_1:1;
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
begin
Lm3:
for R being non empty unital associative multMagma
for a being Element of R
for n, m being Element of NAT holds a |^ (n + m) = (a |^ n) * (a |^ m)
begin
definition
let R be non
empty addLoopStr ;
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
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;
begin