let T be _Tree; :: thesis: for P being Path of T

for a, b being Vertex of T

for i, j being odd Nat st i <= j & j <= len P & P . i = a & P . j = b holds

T .pathBetween (a,b) = P .cut (i,j)

let P be Path of T; :: thesis: for a, b being Vertex of T

for i, j being odd Nat st i <= j & j <= len P & P . i = a & P . j = b holds

T .pathBetween (a,b) = P .cut (i,j)

let a, b be Vertex of T; :: thesis: for i, j being odd Nat st i <= j & j <= len P & P . i = a & P . j = b holds

T .pathBetween (a,b) = P .cut (i,j)

let i, j be odd Nat; :: thesis: ( i <= j & j <= len P & P . i = a & P . j = b implies T .pathBetween (a,b) = P .cut (i,j) )

assume A1: ( i <= j & j <= len P & P . i = a & P . j = b ) ; :: thesis: T .pathBetween (a,b) = P .cut (i,j)

reconsider i9 = i, j9 = j as odd Element of NAT by ORDINAL1:def 12;

P .cut (i9,j9) is_Walk_from a,b by A1, GLIB_001:37;

hence T .pathBetween (a,b) = P .cut (i,j) by Def2; :: thesis: verum

for a, b being Vertex of T

for i, j being odd Nat st i <= j & j <= len P & P . i = a & P . j = b holds

T .pathBetween (a,b) = P .cut (i,j)

let P be Path of T; :: thesis: for a, b being Vertex of T

for i, j being odd Nat st i <= j & j <= len P & P . i = a & P . j = b holds

T .pathBetween (a,b) = P .cut (i,j)

let a, b be Vertex of T; :: thesis: for i, j being odd Nat st i <= j & j <= len P & P . i = a & P . j = b holds

T .pathBetween (a,b) = P .cut (i,j)

let i, j be odd Nat; :: thesis: ( i <= j & j <= len P & P . i = a & P . j = b implies T .pathBetween (a,b) = P .cut (i,j) )

assume A1: ( i <= j & j <= len P & P . i = a & P . j = b ) ; :: thesis: T .pathBetween (a,b) = P .cut (i,j)

reconsider i9 = i, j9 = j as odd Element of NAT by ORDINAL1:def 12;

P .cut (i9,j9) is_Walk_from a,b by A1, GLIB_001:37;

hence T .pathBetween (a,b) = P .cut (i,j) by Def2; :: thesis: verum