let f be non constant standard special_circular_sequence; :: thesis: f /^ 1 is one-to-one
let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x1 in K1((f /^ 1)) or not x2 in K1((f /^ 1)) or not (f /^ 1) . x1 = (f /^ 1) . x2 or x1 = x2 )
assume that
A1:
x1 in dom (f /^ 1)
and
A2:
x2 in dom (f /^ 1)
and
A3:
(f /^ 1) . x1 = (f /^ 1) . x2
; :: thesis: x1 = x2
reconsider i = x1, j = x2 as Element of NAT by A1, A2;
assume A4:
x1 <> x2
; :: thesis: contradiction
A5:
1 <= i
by A1, FINSEQ_3:27;
A6:
1 <= j
by A2, FINSEQ_3:27;
i + 1 in dom f
by A1, FINSEQ_5:29;
then A7:
i + 1 <= len f
by FINSEQ_3:27;
A8:
1 < i + 1
by A5, NAT_1:13;
j + 1 in dom f
by A2, FINSEQ_5:29;
then A9:
( 1 <= j + 1 & j + 1 <= len f )
by FINSEQ_3:27;
A10:
1 < j + 1
by A6, NAT_1:13;