let D be non empty set ; for f being FinSequence of D holds
( f is almost-one-to-one iff ( f /^ 1 is one-to-one & f | ((len f) -' 1) is one-to-one ) )
let f be FinSequence of D; ( f is almost-one-to-one iff ( f /^ 1 is one-to-one & f | ((len f) -' 1) is one-to-one ) )
A1:
len (f /^ 1) = (len f) -' 1
by RFINSEQ:29;
thus
( f is almost-one-to-one implies ( f /^ 1 is one-to-one & f | ((len f) -' 1) is one-to-one ) )
( f /^ 1 is one-to-one & f | ((len f) -' 1) is one-to-one implies f is almost-one-to-one )proof
assume A2:
f is
almost-one-to-one
;
( f /^ 1 is one-to-one & f | ((len f) -' 1) is one-to-one )
thus
f /^ 1 is
one-to-one
f | ((len f) -' 1) is one-to-one proof
let x,
y be
object ;
FUNCT_1:def 4 ( not x in K70((f /^ 1)) or not y in K70((f /^ 1)) or not (f /^ 1) . x = (f /^ 1) . y or x = y )
assume that A3:
x in dom (f /^ 1)
and A4:
y in dom (f /^ 1)
and A5:
(f /^ 1) . x = (f /^ 1) . y
;
x = y
reconsider i =
x,
j =
y as
Nat by A3, A4;
A6:
i in Seg (len (f /^ 1))
by A3, FINSEQ_1:def 3;
then A7:
1
<= i
by FINSEQ_1:1;
A8:
i <= len (f /^ 1)
by A6, FINSEQ_1:1;
then
(len f) -' 1
>= 1
by A1, A7, XXREAL_0:2;
then A9:
(len f) -' 1
= (len f) - 1
by NAT_D:39;
then A10:
i + 1
<= len f
by A1, A8, XREAL_1:19;
then A11:
(f /^ 1) . i = f . (i + 1)
by A7, FINSEQ_6:114;
A12:
j in Seg (len (f /^ 1))
by A4, FINSEQ_1:def 3;
then A13:
1
<= j
by FINSEQ_1:1;
j <= len (f /^ 1)
by A12, FINSEQ_1:1;
then A14:
j + 1
<= len f
by A1, A9, XREAL_1:19;
then A15:
(f /^ 1) . j = f . (j + 1)
by A13, FINSEQ_6:114;
A16:
j + 1
> 1
by A13, NAT_1:13;
then A17:
j + 1
in dom f
by A14, FINSEQ_3:25;
A18:
i + 1
> 1
by A7, NAT_1:13;
then
i + 1
in dom f
by A10, FINSEQ_3:25;
then
i + 1
= j + 1
by A2, A5, A11, A15, A18, A16, A17;
hence
x = y
;
verum
end;
A19:
len (f | ((len f) -' 1)) = (len f) -' 1
by FINSEQ_1:59, NAT_D:35;
thus
f | ((len f) -' 1) is
one-to-one
verumproof
let x,
y be
object ;
FUNCT_1:def 4 ( not x in K70((f | ((len f) -' 1))) or not y in K70((f | ((len f) -' 1))) or not (f | ((len f) -' 1)) . x = (f | ((len f) -' 1)) . y or x = y )
assume that A20:
x in dom (f | ((len f) -' 1))
and A21:
y in dom (f | ((len f) -' 1))
and A22:
(f | ((len f) -' 1)) . x = (f | ((len f) -' 1)) . y
;
x = y
reconsider i =
x,
j =
y as
Nat by A20, A21;
A23:
i in Seg (len (f | ((len f) -' 1)))
by A20, FINSEQ_1:def 3;
then A24:
1
<= i
by FINSEQ_1:1;
A25:
j in Seg (len (f | ((len f) -' 1)))
by A21, FINSEQ_1:def 3;
then A26:
j <= len (f | ((len f) -' 1))
by FINSEQ_1:1;
then A27:
(f | ((len f) -' 1)) . j = f . j
by A19, FINSEQ_3:112;
A28:
i <= len (f | ((len f) -' 1))
by A23, FINSEQ_1:1;
then A29:
(f | ((len f) -' 1)) . i = f . i
by A19, FINSEQ_3:112;
(len f) -' 1
>= 1
by A19, A24, A28, XXREAL_0:2;
then A30:
(len f) -' 1
= (len f) - 1
by NAT_D:39;
then
j + 1
<= len f
by A19, A26, XREAL_1:19;
then A31:
j < len f
by NAT_1:13;
1
<= j
by A25, FINSEQ_1:1;
then A32:
j in dom f
by A31, FINSEQ_3:25;
i + 1
<= len f
by A19, A28, A30, XREAL_1:19;
then A33:
i < len f
by NAT_1:13;
then
i in dom f
by A24, FINSEQ_3:25;
hence
x = y
by A2, A22, A29, A27, A33, A31, A32;
verum
end;
end;
assume that
A34:
f /^ 1 is one-to-one
and
A35:
f | ((len f) -' 1) is one-to-one
; f is almost-one-to-one
let i, j be Nat; JORDAN23:def 1 ( i in dom f & j in dom f & ( i <> 1 or j <> len f ) & ( i <> len f or j <> 1 ) & f . i = f . j implies i = j )
assume that
A36:
i in dom f
and
A37:
j in dom f
and
A38:
( i <> 1 or j <> len f )
and
A39:
( i <> len f or j <> 1 )
and
A40:
f . i = f . j
; i = j
A41:
0 + 1 <= i
by A36, FINSEQ_3:25;
then A42:
i - 1 >= 0
by XREAL_1:19;
A43:
i <= len f
by A36, FINSEQ_3:25;
then A44:
i - 1 <= (len f) - 1
by XREAL_1:9;
then
i -' 1 <= (len f) - 1
by A42, XREAL_0:def 2;
then A45:
i -' 1 <= (len f) -' 1
by XREAL_0:def 2;
len f = ((len f) -' 1) + 1
by A41, A43, XREAL_1:235, XXREAL_0:2;
then
(len f) -' 1 <= len f
by NAT_1:13;
then A46:
len (f | ((len f) -' 1)) = (len f) -' 1
by FINSEQ_1:59;
A47:
j <= len f
by A37, FINSEQ_3:25;
then
j - 1 <= (len f) - 1
by XREAL_1:9;
then
j -' 1 <= (len f) - 1
by A42, A44, XREAL_0:def 2;
then A48:
j -' 1 <= (len f) -' 1
by XREAL_0:def 2;
not f is empty
by A36;
then A49:
f = <*(f /. 1)*> ^ (f /^ 1)
by FINSEQ_5:29;
A50:
i = (i -' 1) + 1
by A41, XREAL_1:235;
A51:
0 + 1 <= j
by A37, FINSEQ_3:25;
then A52:
j - 1 >= 0
by XREAL_1:19;
A53:
j = (j -' 1) + 1
by A51, XREAL_1:235;
per cases
( ( i <> 1 & j <> 1 ) or i = 1 or j = 1 )
;
suppose A54:
(
i <> 1 &
j <> 1 )
;
i = jthen
j > 0 + 1
by A51, XXREAL_0:1;
then
j - 1
> 0
by XREAL_1:20;
then
j -' 1
> 0
by XREAL_0:def 2;
then
j -' 1
>= 0 + 1
by NAT_1:13;
then A55:
j -' 1
in dom (f /^ 1)
by A1, A48, FINSEQ_3:25;
then A56:
f . j = (f /^ 1) . (j -' 1)
by A53, A49, FINSEQ_3:103;
i > 0 + 1
by A41, A54, XXREAL_0:1;
then
i - 1
> 0
by XREAL_1:20;
then
i -' 1
> 0
by XREAL_0:def 2;
then
i -' 1
>= 0 + 1
by NAT_1:13;
then A57:
i -' 1
in dom (f /^ 1)
by A1, A45, FINSEQ_3:25;
then
f . i = (f /^ 1) . (i -' 1)
by A50, A49, FINSEQ_3:103;
then
i -' 1
= j -' 1
by A34, A40, A57, A55, A56;
then
i - 1
= j -' 1
by A42, XREAL_0:def 2;
then
i - 1
= j - 1
by A52, XREAL_0:def 2;
hence
i = j
;
verum end; suppose A58:
i = 1
;
i = jthen
j < len f
by A38, A47, XXREAL_0:1;
then
j + 1
<= len f
by NAT_1:13;
then
j <= (len f) - 1
by XREAL_1:19;
then A59:
j <= (len f) -' 1
by XREAL_0:def 2;
then A60:
(f | ((len f) -' 1)) . j = f . j
by FINSEQ_3:112;
i <= (len f) -' 1
by A51, A58, A59, XXREAL_0:2;
then A61:
i in dom (f | ((len f) -' 1))
by A41, A46, FINSEQ_3:25;
A62:
j in dom (f | ((len f) -' 1))
by A51, A46, A59, FINSEQ_3:25;
(f | ((len f) -' 1)) . i = f . i
by A51, A58, A59, FINSEQ_3:112, XXREAL_0:2;
hence
i = j
by A35, A40, A60, A61, A62;
verum end; suppose A63:
j = 1
;
i = jthen
i < len f
by A39, A43, XXREAL_0:1;
then
i + 1
<= len f
by NAT_1:13;
then
i <= (len f) - 1
by XREAL_1:19;
then A64:
i <= (len f) -' 1
by XREAL_0:def 2;
then A65:
(f | ((len f) -' 1)) . i = f . i
by FINSEQ_3:112;
j <= (len f) -' 1
by A41, A63, A64, XXREAL_0:2;
then A66:
j in dom (f | ((len f) -' 1))
by A51, A46, FINSEQ_3:25;
A67:
i in dom (f | ((len f) -' 1))
by A41, A46, A64, FINSEQ_3:25;
(f | ((len f) -' 1)) . j = f . j
by A41, A63, A64, FINSEQ_3:112, XXREAL_0:2;
hence
i = j
by A35, A40, A65, A67, A66;
verum end;