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

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