let T be _Tree; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( a = a9 & b = b9 implies T .pathBetween (a,b) = t .pathBetween (a9,b9) )
assume that
A1: a = a9 and
A2: b = b9 ; :: thesis: 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; :: thesis: verum