defpred S1[ set , set , set ] means for z being Element of F1() st z = $2 holds
$3 = F4($1,z);
A1:
for n being Nat
for x being Element of F1() ex y being Element of F1() st S1[n,x,y]
proof
let n be
Nat;
for x being Element of F1() ex y being Element of F1() st S1[n,x,y]let x be
Element of
F1();
ex y being Element of F1() st S1[n,x,y]
take
F4(
n,
x)
;
S1[n,x,F4(n,x)]
let z be
Element of
F1();
( z = x implies F4(n,x) = F4(n,z) )
assume
z = x
;
F4(n,x) = F4(n,z)
hence
F4(
n,
x)
= F4(
n,
z)
;
verum
end;
A2:
for n being Nat
for x, y1, y2 being Element of F1() st S1[n,x,y1] & S1[n,x,y2] holds
y1 = y2
proof
let n be
Nat;
for x, y1, y2 being Element of F1() st S1[n,x,y1] & S1[n,x,y2] holds
y1 = y2let x,
y1,
y2 be
Element of
F1();
( S1[n,x,y1] & S1[n,x,y2] implies y1 = y2 )
assume that A3:
for
z being
Element of
F1() st
z = x holds
y1 = F4(
n,
z)
and A4:
for
z being
Element of
F1() st
z = x holds
y2 = F4(
n,
z)
;
y1 = y2
thus y1 =
F4(
n,
x)
by A3
.=
y2
by A4
;
verum
end;
A5:
( ex y being Element of F1() ex f being sequence of F1() st
( y = f . F3() & f . 0 = F2() & ( for n being Nat holds S1[n,f . n,f . (n + 1)] ) ) & ( for y1, y2 being Element of F1() st ex f being sequence of F1() st
( y1 = f . F3() & f . 0 = F2() & ( for n being Nat holds S1[n,f . n,f . (n + 1)] ) ) & ex f being sequence of F1() st
( y2 = f . F3() & f . 0 = F2() & ( for n being Nat holds S1[n,f . n,f . (n + 1)] ) ) holds
y1 = y2 ) )
from RECDEF_1:sch 13(A1, A2);
then consider y being Element of F1(), f being sequence of F1() such that
A6:
( y = f . F3() & f . 0 = F2() )
and
A7:
for n being Nat holds S1[n,f . n,f . (n + 1)]
;
thus
ex y being Element of F1() ex f being sequence of F1() st
( y = f . F3() & f . 0 = F2() & ( for n being Nat holds f . (n + 1) = F4(n,(f . n)) ) )
for y1, y2 being Element of F1() st ex f being sequence of F1() st
( y1 = f . F3() & f . 0 = F2() & ( for n being Nat holds f . (n + 1) = F4(n,(f . n)) ) ) & ex f being sequence of F1() st
( y2 = f . F3() & f . 0 = F2() & ( for n being Nat holds f . (n + 1) = F4(n,(f . n)) ) ) holds
y1 = y2proof
take
y
;
ex f being sequence of F1() st
( y = f . F3() & f . 0 = F2() & ( for n being Nat holds f . (n + 1) = F4(n,(f . n)) ) )
take
f
;
( y = f . F3() & f . 0 = F2() & ( for n being Nat holds f . (n + 1) = F4(n,(f . n)) ) )
thus
(
y = f . F3() &
f . 0 = F2() )
by A6;
for n being Nat holds f . (n + 1) = F4(n,(f . n))
let n be
Nat;
f . (n + 1) = F4(n,(f . n))
reconsider n =
n as
Element of
NAT by ORDINAL1:def 12;
S1[
n,
f . n,
f . (n + 1)]
by A7;
hence
f . (n + 1) = F4(
n,
(f . n))
;
verum
end;
let y1, y2 be Element of F1(); ( ex f being sequence of F1() st
( y1 = f . F3() & f . 0 = F2() & ( for n being Nat holds f . (n + 1) = F4(n,(f . n)) ) ) & ex f being sequence of F1() st
( y2 = f . F3() & f . 0 = F2() & ( for n being Nat holds f . (n + 1) = F4(n,(f . n)) ) ) implies y1 = y2 )
given f being sequence of F1() such that A8:
( y1 = f . F3() & f . 0 = F2() )
and
A9:
for n being Nat holds f . (n + 1) = F4(n,(f . n))
; ( for f being sequence of F1() holds
( not y2 = f . F3() or not f . 0 = F2() or ex n being Nat st not f . (n + 1) = F4(n,(f . n)) ) or y1 = y2 )
A10:
for n being Nat holds S1[n,f . n,f . (n + 1)]
by A9;
given f2 being sequence of F1() such that A11:
( y2 = f2 . F3() & f2 . 0 = F2() )
and
A12:
for n being Nat holds f2 . (n + 1) = F4(n,(f2 . n))
; y1 = y2
for n being Nat holds S1[n,f2 . n,f2 . (n + 1)]
by A12;
hence
y1 = y2
by A5, A8, A11, A10; verum