let G be _Graph; :: thesis: for P, H being Path of G st P .edges() misses H .edges() & not P is trivial & not P is closed & not H is trivial & not H is closed & (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() & not P is trivial & not P is closed & not H is trivial & not H is closed & (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: ( not P is trivial & not P is closed ) and
A3: ( not H is trivial & not H is closed ) and
A4: (P .vertices() ) /\ (H .vertices() ) = {(P .first() ),(P .last() )} and
A5: ( H .first() = P .last() & H .last() = P .first() ) ; :: thesis: P .append H is Cycle-like
set J = P .append H;
A6: ((len (P .append H)) + 1) + (- 1) = ((len P) + (len H)) + (- 1) by A5, GLIB_001:29;

A7: now

let m be odd Nat; :: thesis: ( m <= len P implies (P .append H) . m = P . m )
assume m <= len P ; :: thesis: (P .append H) . m = P . m
then ( 1 <= m & m <= len P ) by HEYTING3:1;
then m in dom P by FINSEQ_3:27;
hence (P .append H) . m = P . m by GLIB_001:33; :: thesis: verum

end;

A8: 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 A9: ( m > len P & m <= len (P .append H) ) ; :: thesis: ( m in dom (P .append H) & not m in dom P )
( 1 <= m & m <= len (P .append H) ) by A9, HEYTING3:1;
hence ( m in dom (P .append H) & not m in dom P ) by A9, FINSEQ_3:27; :: thesis: verum

end;

( (P .append H) .first() = P .first() & (P .append H) .last() = P .first() ) by A5, GLIB_001:31;
then A10: P .append H is closed by GLIB_001:def 24;

now

assume len (P .append H) = 1 ; :: thesis: contradiction
then A11: 1 + 1 = (len P) + (len H) by A5, GLIB_001:29;

now

assume A12: len P <> 1 ; :: thesis: contradiction
1 <= len P by Th2;
then 1 < len P by A12, XXREAL_0:1;
then (len P) + (len H) <= len P by A11, NAT_1:13;
then ((len P) + (len H)) + (- (len P)) <= (len P) + (- (len P)) by XREAL_1:9;
then ( len H <= 0 & 0 <= len H ) ;
hence contradiction ; :: thesis: verum

end;

hence contradiction by A3, A11, GLIB_001:127; :: thesis: verum

end;

then A13: not P .append H is trivial by GLIB_001:127;
( rng (P .edgeSeq() ) = P .edges() & rng (H .edgeSeq() ) = H .edges() & P .edgeSeq() is one-to-one & H .edgeSeq() is one-to-one ) by GLIB_001:def 27;
then (P .edgeSeq() ) ^ (H .edgeSeq() ) is one-to-one by A1, FINSEQ_3:98;
then (P .append H) .edgeSeq() is one-to-one by A5, GLIB_001:86;
then A14: P .append H is Trail-like by GLIB_001:def 27;

now

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 A15: ( m < n & n <= len (P .append H) ) ; :: thesis: ( (P .append H) . b₁ = (P .append H) . b₂ implies ( b₁ = 1 & b₂ = len (P .append H) ) )
A16: ( 1 <= m & m <= len (P .append H) ) by A15, HEYTING3:1, XXREAL_0:2;

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 ( m <= len P & n <= len P ) ; :: thesis: ( (P .append H) . b₁ = (P .append H) . b₂ implies ( b₁ = 1 & b₂ = len (P .append H) ) )

then ( P . m <> P . n & P . m = (P .append H) . m & (P .append H) . n = P . n ) by A2, A7, A15, GLIB_001:148;
hence ( (P .append H) . m = (P .append H) . n implies ( m = 1 & n = len (P .append H) ) ) ; :: thesis: verum

end;

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

then A18: (P .append H) . m = P . m by A7;
( n in dom (P .append H) & not n in dom P ) by A8, A15, A17;
then consider j being Element of NAT such that
A19: ( j < len H & n = (len P) + j ) by GLIB_001:35;
A20: (P .append H) . n = H . (j + 1) by A5, A19, GLIB_001:34;
j is even by A19;
then reconsider jj = j as even Nat ;
reconsider j1 = jj + 1 as odd Nat ;
A21: j1 <= len H by A19, NAT_1:13;

now

assume A22: (P .append H) . m = (P .append H) . n ; :: thesis: ( m = 1 & n = len (P .append H) )
then ( (P .append H) . m in P .vertices() & (P .append H) . m in H .vertices() ) by A17, A18, A20, A21, GLIB_001:88;
then A23: (P .append H) . m in (P .vertices() ) /\ (H .vertices() ) by XBOOLE_0:def 4;

A24: now

assume A25: (P .append H) . m = P .last() ; :: thesis: contradiction
( j <> 0 & 0 <= j ) by A17, A19;
then 0 + 1 < j1 by XREAL_1:10;
then H . ((2 * 0 ) + 1) <> H . j1 by A3, A21, GLIB_001:148;
hence contradiction by A5, A19, A22, A25, GLIB_001:34; :: thesis: verum

end;

then A26: (P .append H) . m = P .first() by A4, A23, TARSKI:def 2;
A27: (P .append H) . n = H .last() by A4, A5, A22, A23, A24, TARSKI:def 2;

A28: now

assume A29: n < len (P .append H) ; :: thesis: contradiction
A30: H . j1 = H . (len H) by A5, A19, A27, GLIB_001:34;
j1 <> len H by A6, A19, A29;
then j1 < len H by A21, XXREAL_0:1;
hence contradiction by A3, A30, GLIB_001:148; :: thesis: verum

end;

now

assume 1 < m ; :: thesis: contradiction
then P . m <> P . ((2 * 0 ) + 1) by A2, A17, GLIB_001:148;
hence contradiction by A7, A17, A26; :: thesis: verum

end;

hence ( m = 1 & n = len (P .append H) ) by A15, A16, A28, 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 A15, XXREAL_0:2; :: thesis: verum

end;

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

then ( m in dom (P .append H) & not m in dom P ) by A8, A16;
then consider k being Element of NAT such that
A32: ( k < len H & m = (len P) + k ) by GLIB_001:35;
( n in dom (P .append H) & not n in dom P ) by A8, A15, A31;
then consider j being Element of NAT such that
A33: ( j < len H & n = (len P) + j ) by GLIB_001:35;
A34: (P .append H) . ((len P) + k) = H . (k + 1) by A5, A32, GLIB_001:34;
A35: (P .append H) . ((len P) + j) = H . (j + 1) by A5, A33, GLIB_001:34;
k is even by A32;
then reconsider kk = k as even Nat ;
reconsider k1 = kk + 1 as odd Nat ;
j is even by A33;
then reconsider jj = j as even Nat ;
reconsider j1 = jj + 1 as odd Element of NAT ;
k < j by A15, A32, A33, XREAL_1:9;
then A36: k1 < j1 by XREAL_1:10;
j1 <= len H by A33, NAT_1:13;
hence ( (P .append H) . m = (P .append H) . n implies ( m = 1 & n = len (P .append H) ) ) by A3, A32, A33, A34, A35, A36, GLIB_001:148; :: thesis: verum

end;

end;

end;

then P .append H is Path-like by A14, GLIB_001:def 28;
hence P .append H is Cycle-like by A10, A13, GLIB_001:def 31; :: thesis: verum