let D be non empty set ; :: thesis: 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; :: thesis: ( 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 JORDAN3:19;
thus
( f is almost-one-to-one implies ( f /^ 1 is one-to-one & f | ((len f) -' 1) is one-to-one ) )
:: thesis: ( 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
;
:: thesis: ( f /^ 1 is one-to-one & f | ((len f) -' 1) is one-to-one )
thus
f /^ 1 is
one-to-one
:: thesis: f | ((len f) -' 1) is one-to-oneproof
let x,
y be
set ;
:: according to FUNCT_1:def 8 :: thesis: ( not x in K1((f /^ 1)) or not y in K1((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
;
:: thesis: x = y
reconsider i =
x,
j =
y as
Element of
NAT by A3, A4;
(
i in Seg (len (f /^ 1)) &
j in Seg (len (f /^ 1)) )
by A3, A4, FINSEQ_1:def 3;
then A6:
( 1
<= i &
i <= len (f /^ 1) & 1
<= j &
j <= len (f /^ 1) )
by FINSEQ_1:3;
then
(len f) -' 1
>= 1
by A1, XXREAL_0:2;
then
(len f) -' 1
= (len f) - 1
by NAT_D:39;
then A7:
(
i + 1
<= len f &
j + 1
<= len f )
by A1, A6, XREAL_1:21;
then A8:
(
(f /^ 1) . i = f . (i + 1) &
(f /^ 1) . j = f . (j + 1) )
by A6, JORDAN3:23;
A9:
(
i + 1
> 1 &
j + 1
> 1 )
by A6, NAT_1:13;
then
(
i + 1
in dom f &
j + 1
in dom f )
by A7, FINSEQ_3:27;
then
i + 1
= j + 1
by A2, A5, A8, A9, Def1;
hence
x = y
;
:: thesis: verum
end;
A10:
len (f | ((len f) -' 1)) = (len f) -' 1
by FINSEQ_1:80, NAT_D:35;
thus
f | ((len f) -' 1) is
one-to-one
:: thesis: verumproof
let x,
y be
set ;
:: according to FUNCT_1:def 8 :: thesis: ( not x in K1((f | ((len f) -' 1))) or not y in K1((f | ((len f) -' 1))) or not (f | ((len f) -' 1)) . x = (f | ((len f) -' 1)) . y or x = y )
assume that A11:
x in dom (f | ((len f) -' 1))
and A12:
y in dom (f | ((len f) -' 1))
and A13:
(f | ((len f) -' 1)) . x = (f | ((len f) -' 1)) . y
;
:: thesis: x = y
reconsider i =
x,
j =
y as
Element of
NAT by A11, A12;
(
i in Seg (len (f | ((len f) -' 1))) &
j in Seg (len (f | ((len f) -' 1))) )
by A11, A12, FINSEQ_1:def 3;
then A14:
( 1
<= i &
i <= len (f | ((len f) -' 1)) & 1
<= j &
j <= len (f | ((len f) -' 1)) )
by FINSEQ_1:3;
then
(len f) -' 1
>= 1
by A10, XXREAL_0:2;
then A15:
(len f) -' 1
= (len f) - 1
by NAT_D:39;
A16:
(
(f | ((len f) -' 1)) . i = f . i &
(f | ((len f) -' 1)) . j = f . j )
by A10, A14, FINSEQ_3:121;
(
i + 1
<= len f &
j + 1
<= len f )
by A10, A14, A15, XREAL_1:21;
then A17:
(
i < len f &
j < len f )
by NAT_1:13;
then
(
i in dom f &
j in dom f )
by A14, FINSEQ_3:27;
hence
x = y
by A2, A13, A16, A17, Def1;
:: thesis: verum
end;
end;
assume that
A18:
f /^ 1 is one-to-one
and
A19:
f | ((len f) -' 1) is one-to-one
; :: thesis: f is almost-one-to-one
let i, j be Element of NAT ; :: according to JORDAN23:def 1 :: thesis: ( 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
A20:
i in dom f
and
A21:
j in dom f
and
A22:
( i <> 1 or j <> len f )
and
A23:
( i <> len f or j <> 1 )
and
A24:
f . i = f . j
; :: thesis: i = j
A25:
( 0 + 1 <= i & i <= len f & 0 + 1 <= j & j <= len f )
by A20, A21, FINSEQ_3:27;
then A26:
( i - 1 >= 0 & j - 1 >= 0 )
by XREAL_1:21;
A28:
( i = (i -' 1) + 1 & j = (j -' 1) + 1 & len f = ((len f) -' 1) + 1 )
by A25, XREAL_1:237, XXREAL_0:2;
( i - 1 <= (len f) - 1 & j - 1 <= (len f) - 1 )
by A25, XREAL_1:11;
then
( i -' 1 <= (len f) - 1 & j -' 1 <= (len f) - 1 )
by A26, XREAL_0:def 2;
then A30:
( i -' 1 <= (len f) -' 1 & j -' 1 <= (len f) -' 1 )
by XREAL_0:def 2;
not f is empty
by A20;
then A31:
f = <*(f /. 1)*> ^ (f /^ 1)
by FINSEQ_5:32;
(len f) -' 1 <= len f
by A28, NAT_1:13;
then A32:
len (f | ((len f) -' 1)) = (len f) -' 1
by FINSEQ_1:80;
per cases
( ( i <> 1 & j <> 1 ) or i = 1 or j = 1 )
;
suppose
(
i <> 1 &
j <> 1 )
;
:: thesis: i = jthen
(
i > 0 + 1 &
j > 0 + 1 )
by A25, XXREAL_0:1;
then
(
i - 1
> 0 &
j - 1
> 0 )
by XREAL_1:22;
then
(
i -' 1
> 0 &
j -' 1
> 0 )
by XREAL_0:def 2;
then
(
i -' 1
>= 0 + 1 &
j -' 1
>= 0 + 1 )
by NAT_1:13;
then A33:
(
i -' 1
in dom (f /^ 1) &
j -' 1
in dom (f /^ 1) )
by A1, A30, FINSEQ_3:27;
then
(
f . i = (f /^ 1) . (i -' 1) &
f . j = (f /^ 1) . (j -' 1) )
by A28, A31, FINSEQ_3:112;
then
i -' 1
= j -' 1
by A18, A24, A33, FUNCT_1:def 8;
then
i - 1
= j -' 1
by A26, XREAL_0:def 2;
then
i - 1
= j - 1
by A26, XREAL_0:def 2;
hence
i = j
;
:: thesis: verum end; suppose A34:
i = 1
;
:: thesis: i = jthen
j < len f
by A22, A25, XXREAL_0:1;
then
j + 1
<= len f
by NAT_1:13;
then
j <= (len f) - 1
by XREAL_1:21;
then A35:
j <= (len f) -' 1
by XREAL_0:def 2;
then A36:
(f | ((len f) -' 1)) . j = f . j
by FINSEQ_3:121;
A37:
i <= (len f) -' 1
by A25, A34, A35, XXREAL_0:2;
A38:
(f | ((len f) -' 1)) . i = f . i
by A25, A34, A35, FINSEQ_3:121, XXREAL_0:2;
(
i in dom (f | ((len f) -' 1)) &
j in dom (f | ((len f) -' 1)) )
by A25, A32, A35, A37, FINSEQ_3:27;
hence
i = j
by A19, A24, A36, A38, FUNCT_1:def 8;
:: thesis: verum end; suppose A39:
j = 1
;
:: thesis: i = jthen
i < len f
by A23, A25, XXREAL_0:1;
then
i + 1
<= len f
by NAT_1:13;
then
i <= (len f) - 1
by XREAL_1:21;
then A40:
i <= (len f) -' 1
by XREAL_0:def 2;
then A41:
(f | ((len f) -' 1)) . i = f . i
by FINSEQ_3:121;
A42:
j <= (len f) -' 1
by A25, A39, A40, XXREAL_0:2;
A43:
(f | ((len f) -' 1)) . j = f . j
by A25, A39, A40, FINSEQ_3:121, XXREAL_0:2;
(
i in dom (f | ((len f) -' 1)) &
j in dom (f | ((len f) -' 1)) )
by A25, A32, A40, A42, FINSEQ_3:27;
hence
i = j
by A19, A24, A41, A43, FUNCT_1:def 8;
:: thesis: verum end;