let f be FinSequence of (TOP-REAL 2); ( f is weakly-one-to-one implies for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f holds
B_Cut (f,p,q) = Rev (B_Cut (f,q,p)) )
assume A1:
f is weakly-one-to-one
; for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f holds
B_Cut (f,p,q) = Rev (B_Cut (f,q,p))
let p, q be Point of (TOP-REAL 2); ( p in L~ f & q in L~ f implies B_Cut (f,p,q) = Rev (B_Cut (f,q,p)) )
assume that
A2:
p in L~ f
and
A3:
q in L~ f
; B_Cut (f,p,q) = Rev (B_Cut (f,q,p))
per cases
( p = q or ( p <> q & ( Index (p,f) < Index (q,f) or ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) ) or ( p <> q & not Index (p,f) < Index (q,f) & not ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) )
;
suppose that A5:
p <> q
and A6:
(
Index (
p,
f)
< Index (
q,
f) or (
Index (
p,
f)
= Index (
q,
f) &
LE p,
q,
f /. (Index (p,f)),
f /. ((Index (p,f)) + 1) ) )
;
B_Cut (f,p,q) = Rev (B_Cut (f,q,p))
( not
Index (
q,
f)
= Index (
p,
f) or not
LE q,
p,
f /. (Index (q,f)),
f /. ((Index (q,f)) + 1) )
by A5, A6, JORDAN3:27;
then A7:
Rev (B_Cut (f,q,p)) = Rev (Rev (R_Cut ((L_Cut (f,p)),q)))
by A6, JORDAN3:def 7;
B_Cut (
f,
p,
q)
= R_Cut (
(L_Cut (f,p)),
q)
by A2, A3, A6, JORDAN3:def 7;
hence
B_Cut (
f,
p,
q)
= Rev (B_Cut (f,q,p))
by A7;
verum end; suppose that
p <> q
and A8:
( not
Index (
p,
f)
< Index (
q,
f) & not (
Index (
p,
f)
= Index (
q,
f) &
LE p,
q,
f /. (Index (p,f)),
f /. ((Index (p,f)) + 1) ) )
;
B_Cut (f,p,q) = Rev (B_Cut (f,q,p))A9:
(
Index (
q,
f)
< Index (
p,
f) or (
Index (
p,
f)
= Index (
q,
f) & not
LE p,
q,
f /. (Index (p,f)),
f /. ((Index (p,f)) + 1) ) )
by A8, XXREAL_0:1;
A10:
now ( Index (p,f) = Index (q,f) & not LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) implies LE q,p,f /. (Index (q,f)),f /. ((Index (q,f)) + 1) )assume that A11:
Index (
p,
f)
= Index (
q,
f)
and A12:
not
LE p,
q,
f /. (Index (p,f)),
f /. ((Index (p,f)) + 1)
;
LE q,p,f /. (Index (q,f)),f /. ((Index (q,f)) + 1)A13:
1
<= Index (
p,
f)
by A2, JORDAN3:8;
A14:
Index (
p,
f)
< len f
by A2, JORDAN3:8;
then A15:
(Index (p,f)) + 1
<= len f
by NAT_1:13;
then A16:
LSeg (
f,
(Index (p,f)))
= LSeg (
(f /. (Index (p,f))),
(f /. ((Index (p,f)) + 1)))
by A13, TOPREAL1:def 3;
then A17:
p in LSeg (
(f /. (Index (p,f))),
(f /. ((Index (p,f)) + 1)))
by A2, JORDAN3:9;
1
<= (Index (p,f)) + 1
by NAT_1:11;
then A18:
(Index (p,f)) + 1
in dom f
by A15, FINSEQ_3:25;
f . (Index (p,f)) <> f . ((Index (p,f)) + 1)
by A1, A13, A14;
then A19:
f . (Index (p,f)) <> f /. ((Index (p,f)) + 1)
by A18, PARTFUN1:def 6;
Index (
p,
f)
in dom f
by A13, A14, FINSEQ_3:25;
then A20:
f /. (Index (p,f)) <> f /. ((Index (p,f)) + 1)
by A19, PARTFUN1:def 6;
q in LSeg (
(f /. (Index (p,f))),
(f /. ((Index (p,f)) + 1)))
by A3, A11, A16, JORDAN3:9;
then
LT q,
p,
f /. (Index (p,f)),
f /. ((Index (p,f)) + 1)
by A12, A17, A20, JORDAN3:28;
hence
LE q,
p,
f /. (Index (q,f)),
f /. ((Index (q,f)) + 1)
by A11, JORDAN3:def 6;
verum end;
B_Cut (
f,
p,
q)
= Rev (R_Cut ((L_Cut (f,q)),p))
by A8, JORDAN3:def 7;
hence
B_Cut (
f,
p,
q)
= Rev (B_Cut (f,q,p))
by A2, A3, A9, A10, JORDAN3:def 7;
verum end; end;