let G be _Graph; :: thesis: for W1, W2 being Walk of G st W1 .last() = W2 .first() holds
(W1 .append W2) .edgeSeq() = (W1 .edgeSeq() ) ^ (W2 .edgeSeq() )
let W1, W2 be Walk of G; :: thesis: ( W1 .last() = W2 .first() implies (W1 .append W2) .edgeSeq() = (W1 .edgeSeq() ) ^ (W2 .edgeSeq() ) )
set W3 = W1 .append W2;
set W4 = (W1 .edgeSeq() ) ^ (W2 .edgeSeq() );
assume A1: W1 .last() = W2 .first() ; :: thesis: (W1 .append W2) .edgeSeq() = (W1 .edgeSeq() ) ^ (W2 .edgeSeq() )
A2: len ((W1 .edgeSeq() ) ^ (W2 .edgeSeq() )) = (len (W1 .edgeSeq() )) + (len (W2 .edgeSeq() )) by FINSEQ_1:35;
(len (W1 .append W2)) + 1 = (len W1) + (len W2) by A1, Lm9;
then (len (W1 .append W2)) + 1 = (len W1) + ((2 * (len (W2 .edgeSeq() ))) + 1) by Def15
.= ((len W1) + (2 * (len (W2 .edgeSeq() )))) + 1 ;
then A3: (2 * (len ((W1 .append W2) .edgeSeq() ))) + 1 = (2 * (len (W2 .edgeSeq() ))) + (len W1) by Def15
.= (2 * (len (W2 .edgeSeq() ))) + ((2 * (len (W1 .edgeSeq() ))) + 1) by Def15
.= ((2 * (len (W2 .edgeSeq() ))) + (2 * (len (W1 .edgeSeq() )))) + 1 ;
A4: W1 .append W2 = W1 ^' W2 by A1, Def10;

now

let n be Nat; :: thesis: ( 1 <= n & n <= len ((W1 .append W2) .edgeSeq() ) implies ((W1 .append W2) .edgeSeq() ) . n = ((W1 .edgeSeq() ) ^ (W2 .edgeSeq() )) . n )
assume A5: ( 1 <= n & n <= len ((W1 .append W2) .edgeSeq() ) ) ; :: thesis: ((W1 .append W2) .edgeSeq() ) . n = ((W1 .edgeSeq() ) ^ (W2 .edgeSeq() )) . n
reconsider n1 = n as Element of NAT by ORDINAL1:def 13;
A6: n1 in dom ((W1 .edgeSeq() ) ^ (W2 .edgeSeq() )) by A2, A3, A5, FINSEQ_3:27;
A7: ((W1 .append W2) .edgeSeq() ) . n1 = (W1 .append W2) . (2 * n1) by A5, Def15;

now

per cases ( n in dom (W1 .edgeSeq() ) or ex k being Nat st
( k in dom (W2 .edgeSeq() ) & n = (len (W1 .edgeSeq() )) + k ) ) by A6, FINSEQ_1:38;

suppose A8: n in dom (W1 .edgeSeq() ) ; :: thesis: ((W1 .append W2) .edgeSeq() ) . n = ((W1 .edgeSeq() ) ^ (W2 .edgeSeq() )) . n

then A9: ( 1 <= n & n <= len (W1 .edgeSeq() ) ) by FINSEQ_3:27;
A10: ((W1 .edgeSeq() ) ^ (W2 .edgeSeq() )) . n = (W1 .edgeSeq() ) . n by A8, FINSEQ_1:def 7
.= W1 . (2 * n) by A9, Def15 ;
2 * n in dom W1 by A8, Lm41;
then ( 1 <= 2 * n & 2 * n <= len W1 ) by FINSEQ_3:27;
hence ((W1 .append W2) .edgeSeq() ) . n = ((W1 .edgeSeq() ) ^ (W2 .edgeSeq() )) . n by A4, A7, A10, GRAPH_2:14; :: thesis: verum

end;

suppose ex k being Nat st
( k in dom (W2 .edgeSeq() ) & n = (len (W1 .edgeSeq() )) + k ) ; :: thesis: ((W1 .append W2) .edgeSeq() ) . n = ((W1 .edgeSeq() ) ^ (W2 .edgeSeq() )) . n

then consider k being Nat such that
A11: ( k in dom (W2 .edgeSeq() ) & n = (len (W1 .edgeSeq() )) + k ) ;
A12: ( 1 <= k & k <= len (W2 .edgeSeq() ) ) by A11, FINSEQ_3:27;
then 1 <= k + k by NAT_1:12;
then reconsider 2kaa1 = (2 * k) - 1 as Element of NAT by INT_1:18;
A13: ((W1 .edgeSeq() ) ^ (W2 .edgeSeq() )) . n = (W2 .edgeSeq() ) . k by A11, FINSEQ_1:def 7
.= W2 . (2 * k) by A12, Def15 ;
(2 * n) + 1 = (2 * k) + ((2 * (len (W1 .edgeSeq() ))) + 1) by A11
.= (2 * k) + (len W1) by Def15 ;
then A14: 2 * n = (len W1) + ((2 * k) - 1) ;
1 + 1 <= k + k by A12, XREAL_1:9;
then A15: (1 + 1) - 1 <= 2kaa1 by XREAL_1:15;
2 * k <= 2 * (len (W2 .edgeSeq() )) by A12, XREAL_1:66;
then 2 * k < (2 * (len (W2 .edgeSeq() ))) + 1 by NAT_1:13;
then 2 * k < len W2 by Def15;
then 2kaa1 < (len W2) - 0 by XREAL_1:16;
then (W1 .append W2) . (2 * n) = W2 . (2kaa1 + 1) by A4, A14, A15, GRAPH_2:15
.= W2 . (2 * k) ;
hence ((W1 .append W2) .edgeSeq() ) . n = ((W1 .edgeSeq() ) ^ (W2 .edgeSeq() )) . n by A5, A13, Def15; :: thesis: verum

end;

end;

end;

hence ((W1 .append W2) .edgeSeq() ) . n = ((W1 .edgeSeq() ) ^ (W2 .edgeSeq() )) . n ; :: thesis: verum

end;

hence (W1 .append W2) .edgeSeq() = (W1 .edgeSeq() ) ^ (W2 .edgeSeq() ) by A2, A3, FINSEQ_1:18; :: thesis: verum