let G be _Graph; :: thesis: for P, H being Path of G st P .edges() misses H .edges() & P is open & H is trivial & H is open & (P .vertices()) /\ (H .vertices()) = {(P .first()),(P .last())} & H .first() = P .last() & H .last() = P .first() holds
P .append H is Cycle-like
let P, H be Path of G; :: thesis: ( P .edges() misses H .edges() & P is open & H is trivial & H is open & (P .vertices()) /\ (H .vertices()) = {(P .first()),(P .last())} & H .first() = P .last() & H .last() = P .first() implies P .append H is Cycle-like )
assume that
A1: P .edges() misses H .edges() and
A2: P is open and
A3: H is trivial and
A4: H is open and
A5: (P .vertices()) /\ (H .vertices()) = {(P .first()),(P .last())} and
A6: H .first() = P .last() and
A7: H .last() = P .first() ; :: thesis: P .append H is Cycle-like
set J = P .append H;
A8: (P .append H) .first() = P .first() by A6, GLIB_001:30;

A9: now :: thesis: for m being odd Nat st m <= len P holds
(P .append H) . m = P . m

let m be odd Nat; :: thesis: ( m <= len P implies (P .append H) . m = P . m )
A10: 1 <= m by ABIAN:12;
assume m <= len P ; :: thesis: (P .append H) . m = P . m
then m in dom P by A10, FINSEQ_3:25;
hence (P .append H) . m = P . m by GLIB_001:32; :: thesis: verum

end;

A11: for m being odd Nat st m > len P & m <= len (P .append H) holds
( m in dom (P .append H) & not m in dom P )

proof

let m be odd Nat; :: thesis: ( m > len P & m <= len (P .append H) implies ( m in dom (P .append H) & not m in dom P ) )
assume that
A12: m > len P and
A13: m <= len (P .append H) ; :: thesis: ( m in dom (P .append H) & not m in dom P )
1 <= m by ABIAN:12;
hence ( m in dom (P .append H) & not m in dom P ) by A12, A13, FINSEQ_3:25; :: thesis: verum

end;

A14: ((len (P .append H)) + 1) + (- 1) = ((len P) + (len H)) + (- 1) by A6, GLIB_001:28;

A15: now :: thesis: for m, n being odd Element of NAT st m < n & n <= len (P .append H) & (P .append H) . m = (P .append H) . n holds
( m = 1 & n = len (P .append H) )

let m, n be odd Element of NAT ; :: thesis: ( m < n & n <= len (P .append H) & (P .append H) . b₁ = (P .append H) . b₂ implies ( b₁ = 1 & b₂ = len (P .append H) ) )
assume that
A16: m < n and
A17: n <= len (P .append H) ; :: thesis: ( (P .append H) . b₁ = (P .append H) . b₂ implies ( b₁ = 1 & b₂ = len (P .append H) ) )
A18: m <= len (P .append H) by A16, A17, XXREAL_0:2;
A19: 1 <= m by ABIAN:12;

per cases ( ( m <= len P & n <= len P ) or ( m <= len P & n > len P ) or ( m > len P & n <= len P ) or ( m > len P & n > len P ) ) ;

suppose A20: ( m <= len P & n <= len P ) ; :: thesis: ( (P .append H) . b₁ = (P .append H) . b₂ implies ( b₁ = 1 & b₂ = len (P .append H) ) )

then A21: P . m = (P .append H) . m by A9;
P . m <> P . n by A2, A16, A20, GLIB_001:147;
hence ( (P .append H) . m = (P .append H) . n implies ( m = 1 & n = len (P .append H) ) ) by A9, A20, A21; :: thesis: verum

end;

suppose A22: ( m <= len P & n > len P ) ; :: thesis: ( (P .append H) . b₁ = (P .append H) . b₂ implies ( b₁ = 1 & b₂ = len (P .append H) ) )

then A23: (P .append H) . m = P . m by A9;
A24: not n in dom P by A11, A17, A22;
n in dom (P .append H) by A11, A17, A22;
then consider j being Element of NAT such that
A25: j < len H and
A26: n = (len P) + j by A24, GLIB_001:34;
reconsider jj = j as even Nat by A26;
reconsider j1 = jj + 1 as odd Nat ;
A27: j1 <= len H by A25, NAT_1:13;
A28: (P .append H) . n = H . (j + 1) by A6, A25, A26, GLIB_001:33;

now :: thesis: ( (P .append H) . m = (P .append H) . n implies ( m = 1 & n = len (P .append H) ) )

assume A29: (P .append H) . m = (P .append H) . n ; :: thesis: ( m = 1 & n = len (P .append H) )

A30: now :: thesis: not (P .append H) . m = P .last()

j <> 0 by A22, A26;
then 0 + 1 < j1 by XREAL_1:8;
then A31: H . ((2 * 0) + 1) <> H . j1 by A4, A27, GLIB_001:147;
assume (P .append H) . m = P .last() ; :: thesis: contradiction
hence contradiction by A6, A25, A26, A29, A31, GLIB_001:33; :: thesis: verum

end;

A32: (P .append H) . m in P .vertices() by A22, A23, GLIB_001:87;
(P .append H) . m in H .vertices() by A28, A27, A29, GLIB_001:87;
then A33: (P .append H) . m in (P .vertices()) /\ (H .vertices()) by A32, XBOOLE_0:def 4;
then A34: (P .append H) . n = H .last() by A5, A7, A29, A30, TARSKI:def 2;

A35: now :: thesis: not n < len (P .append H)

assume n < len (P .append H) ; :: thesis: contradiction
then j1 <> len H by A14, A26;
then A36: j1 < len H by A27, XXREAL_0:1;
H . j1 = H . (len H) by A6, A25, A26, A34, GLIB_001:33;
hence contradiction by A4, A36, GLIB_001:147; :: thesis: verum

end;

A37: (P .append H) . m = P .first() by A5, A33, A30, TARSKI:def 2;

now :: thesis: not 1 < m

assume 1 < m ; :: thesis: contradiction
then P . m <> P . ((2 * 0) + 1) by A2, A22, GLIB_001:147;
hence contradiction by A9, A22, A37; :: thesis: verum

end;

hence ( m = 1 & n = len (P .append H) ) by A17, A19, A35, XXREAL_0:1; :: thesis: verum

end;

hence ( (P .append H) . m = (P .append H) . n implies ( m = 1 & n = len (P .append H) ) ) ; :: thesis: verum

end;

suppose ( m > len P & n <= len P ) ; :: thesis: ( (P .append H) . b₁ = (P .append H) . b₂ implies ( b₁ = 1 & b₂ = len (P .append H) ) )

hence ( (P .append H) . m = (P .append H) . n implies ( m = 1 & n = len (P .append H) ) ) by A16, XXREAL_0:2; :: thesis: verum

end;

suppose A38: ( m > len P & n > len P ) ; :: thesis: ( (P .append H) . b₁ = (P .append H) . b₂ implies ( b₁ = 1 & b₂ = len (P .append H) ) )

then A39: not n in dom P by A11, A17;
n in dom (P .append H) by A11, A17, A38;
then consider j being Element of NAT such that
A40: j < len H and
A41: n = (len P) + j by A39, GLIB_001:34;
reconsider jj = j as even Nat by A41;
reconsider j1 = jj + 1 as odd Element of NAT ;
A42: j1 <= len H by A40, NAT_1:13;
A43: not m in dom P by A11, A18, A38;
m in dom (P .append H) by A11, A18, A38;
then consider k being Element of NAT such that
A44: k < len H and
A45: m = (len P) + k by A43, GLIB_001:34;
reconsider kk = k as even Nat by A45;
reconsider k1 = kk + 1 as odd Nat ;
k < j by A16, A45, A41, XREAL_1:7;
then A46: k1 < j1 by XREAL_1:8;
A47: (P .append H) . ((len P) + j) = H . (j + 1) by A6, A40, GLIB_001:33;
(P .append H) . ((len P) + k) = H . (k + 1) by A6, A44, GLIB_001:33;
hence ( (P .append H) . m = (P .append H) . n implies ( m = 1 & n = len (P .append H) ) ) by A4, A45, A41, A47, A46, A42, GLIB_001:147; :: thesis: verum

end;

end;

end;

A48: H .edgeSeq() is one-to-one by GLIB_001:def 27;

now :: thesis: not len (P .append H) = 1

assume len (P .append H) = 1 ; :: thesis: contradiction
then A49: 1 + 1 = (len P) + (len H) by A6, GLIB_001:28;

now :: thesis: not len P <> 1

assume A50: len P <> 1 ; :: thesis: contradiction
1 <= len P by Th2;
then 1 < len P by A50, XXREAL_0:1;
then (len P) + (len H) <= len P by A49, NAT_1:13;
then ((len P) + (len H)) + (- (len P)) <= (len P) + (- (len P)) by XREAL_1:7;
then len H <= 0 ;
hence contradiction ; :: thesis: verum

end;

hence contradiction by A3, A49, GLIB_001:126; :: thesis: verum

end;

then A51: P .append H is trivial by GLIB_001:126;
(P .append H) .last() = P .first() by A6, A7, GLIB_001:30;
then A52: P .append H is closed by A8;
P .edgeSeq() is one-to-one by GLIB_001:def 27;
then (P .edgeSeq()) ^ (H .edgeSeq()) is one-to-one by A1, A48, FINSEQ_3:91;
then (P .append H) .edgeSeq() is one-to-one by A6, GLIB_001:85;
then P .append H is Trail-like ;
then P .append H is Path-like by A15;
hence P .append H is Cycle-like by A52, A51; :: thesis: verum