let T be _Tree; for a, b being Vertex of T
for t being _Subtree of T
for a9, b9 being Vertex of t st a = a9 & b = b9 holds
T .pathBetween (a,b) = t .pathBetween (a9,b9)
let a, b be Vertex of T; for t being _Subtree of T
for a9, b9 being Vertex of t st a = a9 & b = b9 holds
T .pathBetween (a,b) = t .pathBetween (a9,b9)
let t be _Subtree of T; for a9, b9 being Vertex of t st a = a9 & b = b9 holds
T .pathBetween (a,b) = t .pathBetween (a9,b9)
let a9, b9 be Vertex of t; ( a = a9 & b = b9 implies T .pathBetween (a,b) = t .pathBetween (a9,b9) )
assume that
A1:
a = a9
and
A2:
b = b9
; T .pathBetween (a,b) = t .pathBetween (a9,b9)
set tp = t .pathBetween (a9,b9);
reconsider tp9 = t .pathBetween (a9,b9) as Walk of T by GLIB_001:167;
A3:
t .pathBetween (a9,b9) is_Walk_from a9,b9
by Def2;
A4: tp9 .last() =
(t .pathBetween (a9,b9)) .last()
.=
b
by A2, A3
;
tp9 .first() =
(t .pathBetween (a9,b9)) .first()
.=
a
by A1, A3
;
then
( tp9 is Path-like & tp9 is_Walk_from a,b )
by A4, GLIB_001:176;
hence
T .pathBetween (a,b) = t .pathBetween (a9,b9)
by Def2; verum