let p, q be XFinSequence of ; :: thesis: ( rng p = X & ( for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) & 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 ) implies p = q )
assume that
A25: ( rng p = X & ( for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) ) and
A26: ( 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 ) ) ; :: thesis: p = q
consider k being Nat such that
A6: X c= k by AE221f;
defpred S₁[ XFinSequence] means for X being set st ex k being Nat st X c= k & $1 is XFinSequence of & 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 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;
A27: S₁[ {} ] ;
A28: for p being XFinSequence
for x being set st S₁[p] holds
S₁[p ^ <%x%>]

proof

let p be XFinSequence; :: thesis: for x being set st S₁[p] holds
S₁[p ^ <%x%>]
let x be set ; :: thesis: ( S₁[p] implies S₁[p ^ <%x%>] )
assume A29: S₁[p] ; :: thesis: S₁[p ^ <%x%>]
let X be set ; :: thesis: ( ex k being Nat st X c= k & p ^ <%x%> is XFinSequence of & rng (p ^ <%x%>) = X & ( 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 ) implies for q being XFinSequence of 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 = p ^ <%x%> )
given k being Nat such that A30: X c= k ; :: thesis: ( not p ^ <%x%> is XFinSequence of or not rng (p ^ <%x%>) = X or ex l, m, k1, k2 being Nat st
( l < m & m < len (p ^ <%x%>) & k1 = (p ^ <%x%>) . l & k2 = (p ^ <%x%>) . m & not k1 < k2 ) or for q being XFinSequence of 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 = p ^ <%x%> )
assume A31: ( p ^ <%x%> is XFinSequence of & rng (p ^ <%x%>) = X & ( 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: for q being XFinSequence of 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 = p ^ <%x%>
let q be XFinSequence of ; :: thesis: ( 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 ) implies q = p ^ <%x%> )
assume A32: ( 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 ) ) ; :: thesis: q = p ^ <%x%>
A34: 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 by A31, AFINSQ_1:34;
then rng <%x%> c= NAT by RELAT_1:def 19;
then {x} c= NAT by AFINSQ_1:36;
then reconsider m = x as Element of NAT by ZFMISC_1:37;
take m ; :: thesis: ( m = x & ( for l being Nat st l in X & l <> x holds
l < m ) )
thus m = x ; :: thesis: for l being Nat st l in X & l <> x holds
l < m
thus for l being Nat st l in X & l <> x holds
l < m :: thesis: verum

proof

let l be Nat; :: thesis: ( l in X & l <> x implies l < m )
assume A35: ( l in X & l <> x ) ; :: thesis: l < m
then consider y being set such that
A36: ( y in dom (p ^ <%x%>) & l = (p ^ <%x%>) . y ) by A31, FUNCT_1:def 5;
reconsider k = y as Element of NAT by A36;
k < len (p ^ <%x%>) by A36, NAT_1:45;
then k < (len p) + (len <%x%>) by AFINSQ_1:20;
then k < (len p) + 1 by AFINSQ_1:38;
then A38b: k <= len p by NAT_1:13;
k <> len p by A35, A36, AFINSQ_1:40;
then k < ((len p) + 1) - 1 by A38b, XXREAL_0:1;
then A91: k < ((len p) + (len <%x%>)) - 1 by AFINSQ_1:38;
A92n: len (p ^ <%x%>) < (len (p ^ <%x%>)) + 1 by XREAL_1:31;
A93: len <%x%> = 1 by AFINSQ_1:38;
A39: ( k < (len (p ^ <%x%>)) - 1 & (len (p ^ <%x%>)) - 1 < len (p ^ <%x%>) ) by A91, A92n, AFINSQ_1:20, XREAL_1:21;
A98b: (len (p ^ <%x%>)) -' 1 = (len (p ^ <%x%>)) - 1 by A39, XREAL_0:def 2;
m = (p ^ <%x%>) . (((len p) + (len <%x%>)) - 1) by A93, AFINSQ_1:40
.= (p ^ <%x%>) . ((len (p ^ <%x%>)) - 1) by AFINSQ_1:20 ;
hence l < m by A31, A36, A39, A98b; :: thesis: verum

end;

end;

then reconsider m = x as Nat ;
len q <> 0

proof

assume len q = 0 ; :: thesis: contradiction
then p ^ <%x%> = {} by A31, A32, AFINSQ_1:18, RELAT_1:60;
then 0 = len (p ^ <%x%>)
.= (len p) + (len <%x%>) by AFINSQ_1:20
.= 1 + (len p) by AFINSQ_1:38 ;
hence contradiction ; :: thesis: verum

end;

then consider n being Nat such that
A40: len q = n + 1 by NAT_1:6;
deffunc H₁( Nat) -> Element of REAL = q . $1;
ex q' being XFinSequence st
( len q' = n & ( for m being Element of NAT st m in n holds
q' . m = H₁(m) ) ) from AFINSQ_1:sch 2();
then consider q' being XFinSequence such that
A41b: ( len q' = n & ( for m being Element of NAT st m in n holds
q' . m = q . m ) ) ;
A41n: for m being Nat st m in n holds
q' . m = q . m

proof

let m be Nat; :: thesis: ( m in n implies q' . m = q . m )
assume B1: m in n ; :: thesis: q' . m = q . m
reconsider m2 = m as Element of NAT by ORDINAL1:def 13;
q' . m2 = q . m2 by A41b, B1;
hence q' . m = q . m ; :: thesis: verum

end;

q' is XFinSequence of

proof

now

let x be set ; :: thesis: ( x in rng q' implies x in NAT )
assume x in rng q' ; :: thesis: x in NAT
then consider y being set such that
A42: ( y in dom q' & x = q' . y ) by FUNCT_1:def 5;
reconsider y = y as Element of NAT by A42;
q . y in NAT by ORDINAL1:def 13;
hence x in NAT by A41b, A42; :: thesis: verum

end;

then rng q' c= NAT by TARSKI:def 3;
hence q' is XFinSequence of by RELAT_1:def 19; :: thesis: verum

end;

then reconsider f = q' as XFinSequence of ;
A46: q' ^ <%x%> = q

proof

A47: dom q = (len q') + (len <%x%>) by A41b, A40, AFINSQ_1:38;
for m being Element of NAT st m in dom <%x%> holds
q . ((len q') + m) = <%x%> . m

proof

let m be Element of NAT ; :: thesis: ( m in dom <%x%> implies q . ((len q') + m) = <%x%> . m )
assume m in dom <%x%> ; :: thesis: q . ((len q') + m) = <%x%> . m
then m in len <%x%> ;
then D4: m in 1 by AFINSQ_1:38;
0 + 1 = 0 \/ {0 } by AFINSQ_1:4;
then A50: m = 0 by D4, TARSKI:def 1;
q . ((len q') + m) = x

proof

assume A51n: q . ((len q') + m) <> x ; :: thesis: contradiction
consider d being Nat such that
A52: ( d = x & ( for l being Nat st l in X & l <> x holds
l < d ) ) by A34;
x in rng q

proof

x in {x} by TARSKI:def 1;
then x in rng <%x%> by AFINSQ_1:36;
then x in (rng p) \/ (rng <%x%>) by XBOOLE_0:def 3;
hence x in rng q by A31, A32, AFINSQ_1:29; :: thesis: verum

end;

then consider y being set such that
A53: ( y in dom q & x = q . y ) by FUNCT_1:def 5;
reconsider y = y as Element of NAT by A53;
A76: y < len q by A53, NAT_1:45;
A77: len q < (len q) + 1 by XREAL_1:31;
y + 1 <= len q by A76, NAT_1:13;
then y <= (len q) - 1 by XREAL_1:21;
then A56: ( ( y < (len q) - 1 & (len q) - 1 < len q ) or y = (len q) - 1 ) by A77, XREAL_1:21, XXREAL_0:1;
A57: ( q . ((len q) - 1) is Nat & q . ((len q) - 1) in X )

proof

len q < (len q) + 1 by XREAL_1:31;
then (len q) - 1 < len q by XREAL_1:21;
then A59: (len q) - 1 in dom q by A40, NAT_1:45;
thus q . ((len q) - 1) is Nat ; :: thesis: q . ((len q) - 1) in X
thus q . ((len q) - 1) in X by A32, A59, FUNCT_1:def 5; :: thesis: verum

end;

set k = q . ((len q) - 1);
q . ((len q) - 1) < d by A50, A40, A41b, A51n, A52, A57;
hence contradiction by A32, A52, A53, A56, A40; :: thesis: verum

end;

hence q . ((len q') + m) = <%x%> . m by A50, AFINSQ_1:38; :: thesis: verum

end;

hence q' ^ <%x%> = q by A47, A41b, AFINSQ_1:def 4; :: thesis: verum

end;

q' = p

proof

A60: ex m being Nat st X \ {x} c= m by A30, XBOOLE_1:1;
A61: ( p is XFinSequence of & rng p = X \ {x} & ( for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) )

proof

thus p is XFinSequence of by A31, AFINSQ_1:34; :: thesis: ( rng p = X \ {x} & ( for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) )
thus rng p = X \ {x} :: thesis: for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds
k1 < k2

proof

A62: not x in rng p

proof

assume x in rng p ; :: thesis: contradiction
then consider y being set such that
A63: ( y in dom p & x = p . y ) by FUNCT_1:def 5;
reconsider y = y as Element of NAT by A63;
A66: ( y < len p & len p < len (p ^ <%x%>) )

proof

thus y < len p by A63, NAT_1:45; :: thesis: len p < len (p ^ <%x%>)
(len p) + 1 = (len p) + (len <%x%>) by AFINSQ_1:38
.= len (p ^ <%x%>) by AFINSQ_1:20 ;
hence len p < len (p ^ <%x%>) by XREAL_1:31; :: thesis: verum

end;

A67: m = (p ^ <%x%>) . y by A63, AFINSQ_1:def 4;
m = (p ^ <%x%>) . (len p) by AFINSQ_1:40;
hence contradiction by A31, A66, A67; :: thesis: verum

end;

A68: X = (rng p) \/ (rng <%x%>) by A31, AFINSQ_1:29
.= (rng p) \/ {x} by AFINSQ_1:36 ;
for z being set holds
( z in ((rng p) \/ {x}) \ {x} iff z in rng p )

proof

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

proof

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

end;

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

end;

hence rng p = X \ {x} by A68, TARSKI:2; :: thesis: verum

end;

thus for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds
k1 < k2 :: thesis: verum

proof

let l, m, k1, k2 be Nat; :: thesis: ( l < m & m < len p & k1 = p . l & k2 = p . m implies k1 < k2 )
assume A71: ( l < m & m < len p & k1 = p . l & k2 = p . m ) ; :: thesis: k1 < k2
then l < len p by XXREAL_0:2;
then l in dom p by NAT_1:45;
then A72: k1 = (p ^ <%x%>) . l by A71, AFINSQ_1:def 4;
m in dom p by A71, NAT_1:45;
then A73: k2 = (p ^ <%x%>) . m by A71, AFINSQ_1:def 4;
len p < (len p) + 1 by XREAL_1:31;
then m < (len p) + 1 by A71, XXREAL_0:2;
then m < (len p) + (len <%x%>) by AFINSQ_1:38;
then ( l < m & m < len (p ^ <%x%>) ) by A71, AFINSQ_1:20;
hence k1 < k2 by A31, A72, A73; :: thesis: verum

end;

end;

( rng f = X \ {x} & ( for l, m, k1, k2 being Nat st l < m & m < len f & k1 = f . l & k2 = f . m holds
k1 < k2 ) )

proof

thus rng f = X \ {x} :: thesis: for l, m, k1, k2 being Nat st l < m & m < len f & k1 = f . l & k2 = f . m holds
k1 < k2

proof

A74: not x in rng f

proof

assume x in rng f ; :: thesis: contradiction
then consider y being set such that
A75: ( y in dom f & x = f . y ) by FUNCT_1:def 5;
reconsider y = y as Element of NAT by A75;
A78: ( y < len f & len f < len (f ^ <%x%>) )

proof

thus y < len f by A75, NAT_1:45; :: thesis: len f < len (f ^ <%x%>)
(len f) + 1 = (len f) + (len <%x%>) by AFINSQ_1:38
.= len (f ^ <%x%>) by AFINSQ_1:20 ;
hence len f < len (f ^ <%x%>) by XREAL_1:31; :: thesis: verum

end;

A79: m = q . y by A46, A75, AFINSQ_1:def 4;
m = q . (len f) by A46, AFINSQ_1:40;
hence contradiction by A32, A46, A78, A79; :: thesis: verum

end;

A80: X = (rng f) \/ (rng <%x%>) by A32, A46, AFINSQ_1:29
.= (rng f) \/ {x} by AFINSQ_1:36 ;
for z being set holds
( z in ((rng f) \/ {x}) \ {x} iff z in rng f )

proof

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

proof

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

end;

assume A81: z in rng f ; :: thesis: z in ((rng f) \/ {x}) \ {x}
then A82: not z in {x} by A74, TARSKI:def 1;
z in (rng f) \/ {x} by A81, XBOOLE_0:def 3;
hence z in ((rng f) \/ {x}) \ {x} by A82, XBOOLE_0:def 5; :: thesis: verum

end;

hence rng f = X \ {x} by A80, TARSKI:2; :: thesis: verum

end;

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

proof

let l, m, k1, k2 be Nat; :: thesis: ( l < m & m < len f & k1 = f . l & k2 = f . m implies k1 < k2 )
assume A83: ( l < m & m < len f & k1 = f . l & k2 = f . m ) ; :: thesis: k1 < k2
then A84: ( l < m & m < len q ) by A40, A41b, NAT_1:13;
( l in n & m in n )

proof

l < n by A41b, A83, XXREAL_0:2;
hence l in n by NAT_1:45; :: thesis: m in n
thus m in n by A41b, A83, NAT_1:45; :: thesis: verum

end;

then ( k1 = q . l & k2 = q . m ) by A41n, A83;
hence k1 < k2 by A32, A84; :: thesis: verum

end;

end;

hence q' = p by A29, A60, A61; :: thesis: verum

end;

hence q = p ^ <%x%> by A46; :: thesis: verum

end;

for p being XFinSequence holds S₁[p] from AFINSQ_1:sch 3(A27, A28);
hence p = q by A6, A25, A26; :: thesis: verum