defpred S₁[ XFinSequence] means for X being set st ex k being Nat st X c= k & $1 is XFinSequence of NAT & rng $1 = X & ( for l, m, k1, k2 being Nat st l < m & m < len $1 & k1 = $1 . l & k2 = $1 . m holds
k1 < k2 ) holds
for q being XFinSequence of NAT st rng q = X & ( for l, m, k1, k2 being Nat st l < m & m < len q & k1 = q . l & k2 = q . m holds
k1 < k2 ) holds
q = $1;
let p, q be XFinSequence of NAT ; :: thesis:
assume that
A31: rng p = X and
A32: for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds
k1 < k2 and
A33: rng q = X and
A34: for l, m, k1, k2 being Nat st l < m & m < len q & k1 = q . l & k2 = q . m holds
k1 < k2 ; :: thesis:
A35: for p being XFinSequence
for x being object st S₁[p] holds
S₁[p ^ <%x%>]

let p be XFinSequence; :: thesis:
let x be object ; :: thesis:
assume A36: S₁[p] ; :: thesis:
let X be set ; :: thesis:
given k being Nat such that A37: X c= k ; :: thesis:
assume that
A38: p ^ <%x%> is XFinSequence of NAT and
A39: rng (p ^ <%x%>) = X and
A40: for l, m, k1, k2 being Nat st l < m & m < len (p ^ <%x%>) & k1 = (p ^ <%x%>) . l & k2 = (p ^ <%x%>) . m holds
k1 < k2 ; :: thesis:
let q be XFinSequence of NAT ; :: thesis:
assume that
A41: rng q = X and
A42: for l, m, k1, k2 being Nat st l < m & m < len q & k1 = q . l & k2 = q . m holds
k1 < k2 ; :: thesis:
deffunc H₁( Nat) -> Element of omega = q . $1;
len q <> 0

assume len q = 0 ; :: thesis:
then p ^ <%x%> = {} by A39, A41, AFINSQ_1:15, RELAT_1:38;
then 0 = len (p ^ <%x%>)
.= (len p) + (len <%x%>) by AFINSQ_1:17
.= 1 + (len p) by AFINSQ_1:34 ;
hence contradiction ; :: thesis:

end;

then consider n being Nat such that
A43: len q = n + 1 by NAT_1:6;
A44: ex m being Nat st
( m = x & ( for l being Nat st l in X & l <> x holds
l < m ) )

proof

<%x%> is XFinSequence of NAT by A38, AFINSQ_1:31;
then rng <%x%> c= NAT by RELAT_1:def 19;
then {x} c= NAT by AFINSQ_1:33;
then reconsider m = x as Element of NAT by ZFMISC_1:31;
take m ; :: thesis:
thus m = x ; :: thesis:
thus for l being Nat st l in X & l <> x holds
l < m :: thesis:

proof

len <%x%> = 1 by AFINSQ_1:34;
then A45: m = (p ^ <%x%>) . (((len p) + (len <%x%>)) - 1) by AFINSQ_1:36
.= (p ^ <%x%>) . ((len (p ^ <%x%>)) - 1) by AFINSQ_1:17 ;
len (p ^ <%x%>) < (len (p ^ <%x%>)) + 1 by XREAL_1:29;
then A46: (len (p ^ <%x%>)) - 1 < len (p ^ <%x%>) by XREAL_1:19;
let l be Nat; :: thesis:
assume that
A47: l in X and
A48: l <> x ; :: thesis:
consider y being object such that
A49: y in dom (p ^ <%x%>) and
A50: l = (p ^ <%x%>) . y by A39, A47, FUNCT_1:def 3;
reconsider k = y as Element of NAT by A49;
k < len (p ^ <%x%>) by A49, AFINSQ_1:86;
then k < (len p) + (len <%x%>) by AFINSQ_1:17;
then k < (len p) + 1 by AFINSQ_1:34;
then A51: k <= len p by NAT_1:13;
k <> len p by A48, A50, AFINSQ_1:36;
then k < ((len p) + 1) - 1 by A51, XXREAL_0:1;
then k < ((len p) + (len <%x%>)) - 1 by AFINSQ_1:34;
then A52: k < (len (p ^ <%x%>)) - 1 by AFINSQ_1:17;
then (len (p ^ <%x%>)) -' 1 = (len (p ^ <%x%>)) - 1 by XREAL_0:def 2;
hence l < m by A40, A50, A52, A46, A45; :: thesis:

end;

then reconsider m = x as Nat ;
A53: not x in rng p

proof

(len p) + 1 = (len p) + (len <%x%>) by AFINSQ_1:34
.= len (p ^ <%x%>) by AFINSQ_1:17 ;
then A54: len p < len (p ^ <%x%>) by XREAL_1:29;
A55: m = (p ^ <%x%>) . (len p) by AFINSQ_1:36;
assume x in rng p ; :: thesis:
then consider y being object such that
A56: y in dom p and
A57: x = p . y by FUNCT_1:def 3;
reconsider y = y as Element of NAT by A56;
A58: y < len p by A56, AFINSQ_1:86;
m = (p ^ <%x%>) . y by A56, A57, AFINSQ_1:def 3;
hence contradiction by A40, A58, A54, A55; :: thesis:

end;

A59: for z being object holds
( z in ((rng p) \/ {x}) \ {x} iff z in rng p )

proof

let z be object ; :: thesis:
thus ( z in ((rng p) \/ {x}) \ {x} implies z in rng p ) :: thesis:

proof

assume A60: z in ((rng p) \/ {x}) \ {x} ; :: thesis:
then not z in {x} by XBOOLE_0:def 5;
hence z in rng p by A60, XBOOLE_0:def 3; :: thesis:

end;

assume A61: z in rng p ; :: thesis:
then A62: z in (rng p) \/ {x} by XBOOLE_0:def 3;
not z in {x} by A53, A61, TARSKI:def 1;
hence z in ((rng p) \/ {x}) \ {x} by A62, XBOOLE_0:def 5; :: thesis:

end;

deffunc H₂( set ) -> Element of omega = q . $1;
consider q9 being XFinSequence such that
A63: len q9 = n and
A64: for m being Nat st m in n holds
q9 . m = H₂(m) from AFINSQ_1:sch 2();

now :: thesis:

let x be object ; :: thesis:
assume x in rng q9 ; :: thesis:
then consider y being object such that
A65: y in dom q9 and
A66: x = q9 . y by FUNCT_1:def 3;
reconsider y = y as Element of NAT by A65;
q . y in NAT ;
hence x in NAT by A63, A64, A65, A66; :: thesis:

end;

then rng q9 c= NAT ;
then reconsider f = q9 as XFinSequence of NAT by RELAT_1:def 19;
A67: p is XFinSequence of NAT by A38, AFINSQ_1:31;
A68: for m being Nat st m in dom <%x%> holds
q . ((len q9) + m) = <%x%> . m

proof

let m be Nat; :: thesis:
assume m in dom <%x%> ; :: thesis:
then m in len <%x%> ;
then A69: m in 1 by AFINSQ_1:34;
Segm (0 + 1) = (Segm 0) \/ {0} by AFINSQ_1:2;
then A70: m = 0 by A69, TARSKI:def 1;
q . ((len q9) + m) = x

proof

x in {x} by TARSKI:def 1;
then x in rng <%x%> by AFINSQ_1:33;
then x in (rng p) \/ (rng <%x%>) by XBOOLE_0:def 3;
then x in rng q by A39, A41, AFINSQ_1:26;
then consider y being object such that
A71: y in dom q and
A72: x = q . y by FUNCT_1:def 3;
reconsider y = y as Element of NAT by A71;
y + 1 <= len q by NAT_1:13, A71, AFINSQ_1:86;
then A73: y <= (len q) - 1 by XREAL_1:19;
len q < (len q) + 1 by XREAL_1:29;
then (len q) - 1 in dom q by A43, AFINSQ_1:86, XREAL_1:19;
then A74: q . ((len q) - 1) in X by A41, FUNCT_1:def 3;
len q < (len q) + 1 by XREAL_1:29;
then A75: ( ( y < (len q) - 1 & (len q) - 1 < len q ) or y = (len q) - 1 ) by A73, XREAL_1:19, XXREAL_0:1;
set k = q . ((len q) - 1);
consider d being Nat such that
A76: d = x and
A77: for l being Nat st l in X & l <> x holds
l < d by A44;
assume q . ((len q9) + m) <> x ; :: thesis:
then q . ((len q) - 1) < d by A43, A63, A70, A77, A74;
hence contradiction by A42, A43, A76, A72, A75; :: thesis:

end;

hence q . ((len q9) + m) = <%x%> . m by A70; :: thesis:

end;

A78: dom q = (len q9) + (len <%x%>) by A43, A63, AFINSQ_1:34;
then A79: q9 ^ <%x%> = q by A63, A64, A68, AFINSQ_1:def 3;
A80: not x in rng f

proof

(len f) + 1 = (len f) + (len <%x%>) by AFINSQ_1:34
.= len (f ^ <%x%>) by AFINSQ_1:17 ;
then A81: len f < len (f ^ <%x%>) by XREAL_1:29;
A82: m = q . (len f) by A79, AFINSQ_1:36;
assume x in rng f ; :: thesis:
then consider y being object such that
A83: y in dom f and
A84: x = f . y by FUNCT_1:def 3;
reconsider y = y as Element of NAT by A83;
A85: y < len f by A83, AFINSQ_1:86;
m = q . y by A63, A64, A83, A84;
hence contradiction by A42, A79, A85, A81, A82; :: thesis:

end;

A86: for z being object holds
( z in ((rng f) \/ {x}) \ {x} iff z in rng f )

proof

let z be object ; :: thesis:
thus ( z in ((rng f) \/ {x}) \ {x} implies z in rng f ) :: thesis:

proof

assume A87: z in ((rng f) \/ {x}) \ {x} ; :: thesis:
then not z in {x} by XBOOLE_0:def 5;
hence z in rng f by A87, XBOOLE_0:def 3; :: thesis:

end;

assume A88: z in rng f ; :: thesis:
then A89: z in (rng f) \/ {x} by XBOOLE_0:def 3;
not z in {x} by A80, A88, TARSKI:def 1;
hence z in ((rng f) \/ {x}) \ {x} by A89, XBOOLE_0:def 5; :: thesis:

end;

X = (rng p) \/ (rng <%x%>) by A39, AFINSQ_1:26
.= (rng p) \/ {x} by AFINSQ_1:33 ;
then A90: rng p = X \ {x} by A59, TARSKI:2;
A91: for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds
k1 < k2

proof

let l, m, k1, k2 be Nat; :: thesis:
assume that
A92: l < m and
A93: m < len p and
A94: k1 = p . l and
A95: k2 = p . m ; :: thesis:
l < len p by A92, A93, XXREAL_0:2;
then l in dom p by AFINSQ_1:86;
then A96: k1 = (p ^ <%x%>) . l by A94, AFINSQ_1:def 3;
len p < (len p) + 1 by XREAL_1:29;
then m < (len p) + 1 by A93, XXREAL_0:2;
then m < (len p) + (len <%x%>) by AFINSQ_1:34;
then A97: m < len (p ^ <%x%>) by AFINSQ_1:17;
m in dom p by A93, AFINSQ_1:86;
then k2 = (p ^ <%x%>) . m by A95, AFINSQ_1:def 3;
hence k1 < k2 by A40, A92, A96, A97; :: thesis:

end;

A98: for l, m, k1, k2 being Nat st l < m & m < len f & k1 = f . l & k2 = f . m holds
k1 < k2

proof

let l, m, k1, k2 be Nat; :: thesis:
assume that
A99: l < m and
A100: m < len f and
A101: k1 = f . l and
A102: k2 = f . m ; :: thesis:
A103: k2 = q . m by A64, A102, A63, A100, AFINSQ_1:86;
l < n by A63, A99, A100, XXREAL_0:2;
then l in Segm n by NAT_1:44;
then A104: k1 = q . l by A64, A101;
m < len q by A43, A63, A100, NAT_1:13;
hence k1 < k2 by A42, A99, A104, A103; :: thesis:

end;

X = (rng f) \/ (rng <%x%>) by A41, A79, AFINSQ_1:26
.= (rng f) \/ {x} by AFINSQ_1:33 ;
then A105: rng f = X \ {x} by A86, TARSKI:2;
ex m being Nat st X \ {x} c= m by A37, XBOOLE_1:1;
then q9 = p by A36, A91, A67, A90, A98, A105;
hence q = p ^ <%x%> by A63, A64, A78, A68, AFINSQ_1:def 3; :: thesis:

end;

A106: S₁[ {} ] ;
A107: for p being XFinSequence holds S₁[p] from AFINSQ_1:sch 3(A106, A35);
ex k being Nat st X c= Segm k by Th2;
hence p = q by A31, A32, A33, A34, A107; :: thesis: