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