let p, q be FinSequence; for G being Graph st p ^ q is oriented Simple Chain of G holds
( p is oriented Simple Chain of G & q is oriented Simple Chain of G )
let G be Graph; ( p ^ q is oriented Simple Chain of G implies ( p is oriented Simple Chain of G & q is oriented Simple Chain of G ) )
assume A1:
p ^ q is oriented Simple Chain of G
; ( p is oriented Simple Chain of G & q is oriented Simple Chain of G )
set r = p ^ q;
per cases
( p = {} or q = {} or ( not p = {} & not q = {} ) )
;
suppose A3:
( not
p = {} & not
q = {} )
;
( p is oriented Simple Chain of G & q is oriented Simple Chain of G )consider vs being
FinSequence of the
carrier of
G such that A4:
vs is_oriented_vertex_seq_of p ^ q
and A5:
for
n,
m being
Nat st 1
<= n &
n < m &
m <= len vs &
vs . n = vs . m holds
(
n = 1 &
m = len vs )
by A1, GRAPH_4:def 7;
A6:
len vs = (len (p ^ q)) + 1
by A4, GRAPH_4:def 5;
A7:
len (p ^ q) = (len p) + (len q)
by FINSEQ_1:22;
then A8:
len vs = ((len p) + 1) + (len q)
by A6;
then consider f1,
f2 being
FinSequence such that A9:
len f1 = (len p) + 1
and
len f2 = len q
and A10:
vs = f1 ^ f2
by FINSEQ_2:22;
A11:
len vs = (len p) + ((len q) + 1)
by A6, A7;
then consider h1,
h2 being
FinSequence such that A12:
len h1 = len p
and A13:
len h2 = (len q) + 1
and A14:
vs = h1 ^ h2
by FINSEQ_2:22;
reconsider f1 =
f1 as
FinSequence of the
carrier of
G by A10, FINSEQ_1:36;
A15:
now for n, m being Nat st 1 <= n & n < m & m <= len f1 & f1 . n = f1 . m holds
( n = 1 & m = len f1 )let n,
m be
Nat;
( 1 <= n & n < m & m <= len f1 & f1 . n = f1 . m implies ( n = 1 & m = len f1 ) )assume that A16:
1
<= n
and A17:
n < m
and A18:
m <= len f1
and A19:
f1 . n = f1 . m
;
( n = 1 & m = len f1 )
n <= len f1
by A17, A18, XXREAL_0:2;
then A20:
f1 . n = vs . n
by A10, A16, Lm1;
1
<= m
by A16, A17, XXREAL_0:2;
then A21:
f1 . m = vs . m
by A10, A18, Lm1;
assume
( not
n = 1 or not
m = len f1 )
;
contradiction
(len f1) + 0 < len vs
by A3, A8, A9, XREAL_1:8;
then
m < len vs
by A18, XXREAL_0:2;
hence
contradiction
by A5, A16, A17, A19, A20, A21;
verum end; reconsider h2 =
h2 as
FinSequence of the
carrier of
G by A14, FINSEQ_1:36;
now for n being Nat st 1 <= n & n <= len q holds
q . n orientedly_joins h2 /. n,h2 /. (n + 1)let n be
Nat;
( 1 <= n & n <= len q implies q . n orientedly_joins h2 /. n,h2 /. (n + 1) )assume that A22:
1
<= n
and A23:
n <= len q
;
q . n orientedly_joins h2 /. n,h2 /. (n + 1)set m =
(len p) + n;
A24:
(len p) + n <= len (p ^ q)
by A7, A23, XREAL_1:7;
then
( 1
<= ((len p) + n) + 1 &
((len p) + n) + 1
<= len vs )
by A6, NAT_1:11, XREAL_1:7;
then A25:
((len p) + n) + 1
in dom vs
by FINSEQ_3:25;
A26:
1
<= n + 1
by NAT_1:11;
n + 1
<= len h2
by A13, A23, XREAL_1:7;
then
n + 1
in dom h2
by A26, FINSEQ_3:25;
then A27:
h2 /. (n + 1) =
h2 . (n + 1)
by PARTFUN1:def 6
.=
vs . ((len h1) + (n + 1))
by A13, A14, A23, A26, Lm2, XREAL_1:7
.=
vs /. (((len p) + n) + 1)
by A12, A25, PARTFUN1:def 6
;
n <= (len p) + n
by NAT_1:11;
then A28:
1
<= (len p) + n
by A22, XXREAL_0:2;
len (p ^ q) <= len vs
by A6, NAT_1:11;
then
(len p) + n <= len vs
by A24, XXREAL_0:2;
then A29:
(len p) + n in dom vs
by A28, FINSEQ_3:25;
A30:
n + 0 <= len h2
by A13, A23, XREAL_1:7;
then
n in dom h2
by A22, FINSEQ_3:25;
then A31:
h2 /. n =
h2 . n
by PARTFUN1:def 6
.=
vs . ((len p) + n)
by A12, A14, A22, A30, Lm2
.=
vs /. ((len p) + n)
by A29, PARTFUN1:def 6
;
(p ^ q) . ((len p) + n) orientedly_joins vs /. ((len p) + n),
vs /. (((len p) + n) + 1)
by A4, A24, A28, GRAPH_4:def 5;
hence
q . n orientedly_joins h2 /. n,
h2 /. (n + 1)
by A22, A23, A31, A27, Lm2;
verum end; then A32:
h2 is_oriented_vertex_seq_of q
by A13, GRAPH_4:def 5;
now for n being Nat st 1 <= n & n <= len p holds
p . n orientedly_joins f1 /. n,f1 /. (n + 1)let n be
Nat;
( 1 <= n & n <= len p implies p . n orientedly_joins f1 /. n,f1 /. (n + 1) )assume that A33:
1
<= n
and A34:
n <= len p
;
p . n orientedly_joins f1 /. n,f1 /. (n + 1)A35:
1
<= n + 1
by NAT_1:11;
len p <= len (p ^ q)
by A7, NAT_1:11;
then A36:
n <= len (p ^ q)
by A34, XXREAL_0:2;
then
n + 1
<= len vs
by A6, XREAL_1:7;
then A37:
n + 1
in dom vs
by A35, FINSEQ_3:25;
len p <= len vs
by A11, NAT_1:11;
then
n <= len vs
by A34, XXREAL_0:2;
then A38:
n in dom vs
by A33, FINSEQ_3:25;
A39:
n + 0 <= len f1
by A9, A34, XREAL_1:7;
then
n in dom f1
by A33, FINSEQ_3:25;
then A40:
f1 /. n =
f1 . n
by PARTFUN1:def 6
.=
vs . n
by A10, A33, A39, Lm1
.=
vs /. n
by A38, PARTFUN1:def 6
;
n + 1
<= len f1
by A9, A34, XREAL_1:7;
then
n + 1
in dom f1
by A35, FINSEQ_3:25;
then A41:
f1 /. (n + 1) =
f1 . (n + 1)
by PARTFUN1:def 6
.=
vs . (n + 1)
by A9, A10, A34, A35, Lm1, XREAL_1:7
.=
vs /. (n + 1)
by A37, PARTFUN1:def 6
;
(p ^ q) . n orientedly_joins vs /. n,
vs /. (n + 1)
by A4, A33, A36, GRAPH_4:def 5;
hence
p . n orientedly_joins f1 /. n,
f1 /. (n + 1)
by A33, A34, A40, A41, Lm1;
verum end; then
f1 is_oriented_vertex_seq_of p
by A9, GRAPH_4:def 5;
hence
p is
oriented Simple Chain of
G
by A1, A15, Th9, GRAPH_4:def 7;
q is oriented Simple Chain of Gnow for n, m being Nat st 1 <= n & n < m & m <= len h2 & h2 . n = h2 . m holds
( n = 1 & m = len h2 )let n,
m be
Nat;
( 1 <= n & n < m & m <= len h2 & h2 . n = h2 . m implies ( n = 1 & m = len h2 ) )assume that A42:
1
<= n
and A43:
n < m
and A44:
m <= len h2
and A45:
h2 . n = h2 . m
;
( n = 1 & m = len h2 )
n <= len h2
by A43, A44, XXREAL_0:2;
then A46:
h2 . n = vs . ((len h1) + n)
by A14, A42, Lm2;
assume
( not
n = 1 or not
m = len h2 )
;
contradictionA47:
(len h1) + m <= len vs
by A11, A12, A13, A44, XREAL_1:7;
1
<= m
by A42, A43, XXREAL_0:2;
then A48:
h2 . m = vs . ((len h1) + m)
by A14, A44, Lm2;
(
0 + 1
< (len h1) + n &
(len h1) + n < (len h1) + m )
by A3, A12, A42, A43, XREAL_1:8;
hence
contradiction
by A5, A45, A46, A48, A47;
verum end; hence
q is
oriented Simple Chain of
G
by A1, A32, Th9, GRAPH_4:def 7;
verum end;