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