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:168;
A3: t .pathBetween a9,b9 is_Walk_from a9,b9 by Def2;
A4: tp9 .last() = (t .pathBetween a9,b9) .last()
.= b by A2, A3, GLIB_001:def 23 ;
tp9 .first() = (t .pathBetween a9,b9) .first()
.= a by A1, A3, GLIB_001:def 23 ;
then ( tp9 is Path-like & tp9 is_Walk_from a,b ) by A4, GLIB_001:177, GLIB_001:def 23;
hence T .pathBetween a,b = t .pathBetween a9,b9 by Def2; :: thesis: verum