let f1, f2 be Function; ( dom f1 = dom f & ( for a being set st a in dom f holds
( ( f orbit a c= A implies f1 . a = x ) & ( for n being Nat st (iter (f,n)) . a nin A & ( for i being Nat st i < n holds
(iter (f,i)) . a in A ) holds
f1 . a = (iter (f,n)) . a ) ) ) & dom f2 = dom f & ( for a being set st a in dom f holds
( ( f orbit a c= A implies f2 . a = x ) & ( for n being Nat st (iter (f,n)) . a nin A & ( for i being Nat st i < n holds
(iter (f,i)) . a in A ) holds
f2 . a = (iter (f,n)) . a ) ) ) implies f1 = f2 )
assume that
A33:
dom f1 = dom f
and
A34:
for a being set st a in dom f holds
( ( f orbit a c= A implies f1 . a = x ) & ( for n being Nat st (iter (f,n)) . a nin A & ( for i being Nat st i < n holds
(iter (f,i)) . a in A ) holds
f1 . a = (iter (f,n)) . a ) )
and
A35:
dom f2 = dom f
and
A36:
for a being set st a in dom f holds
( ( f orbit a c= A implies f2 . a = x ) & ( for n being Nat st (iter (f,n)) . a nin A & ( for i being Nat st i < n holds
(iter (f,i)) . a in A ) holds
f2 . a = (iter (f,n)) . a ) )
; f1 = f2
now for a being object st a in dom f holds
f1 . a = f2 . alet a be
object ;
( a in dom f implies f1 . b1 = f2 . b1 )assume A37:
a in dom f
;
f1 . b1 = f2 . b1per cases
( f orbit a c= A or not f orbit a c= A )
;
suppose
not
f orbit a c= A
;
f1 . b1 = f2 . b1then consider y being
object such that A39:
y in f orbit a
and A40:
y nin A
;
A41:
ex
n1 being
Element of
NAT st
(
y = (iter (f,n1)) . a &
a in dom (iter (f,n1)) )
by A39;
defpred S2[
Nat]
means (iter (f,$1)) . a nin A;
A42:
ex
n being
Nat st
S2[
n]
by A40, A41;
consider n being
Nat such that A43:
S2[
n]
and A44:
for
m being
Nat st
S2[
m] holds
n <= m
from NAT_1:sch 5(A42);
A45:
for
i being
Nat st
i < n holds
(iter (f,i)) . a in A
by A44;
hence f1 . a =
(iter (f,n)) . a
by A34, A37, A43
.=
f2 . a
by A36, A37, A43, A45
;
verum end; end; end;
hence
f1 = f2
by A33, A35; verum