let IT1, IT2 be FF:ELabeling of G; :: thesis: ( ( for e being set st e in the_Edges_of G & not e in P .edges() holds
IT1 . e = EL . e ) & ( for n being odd Nat st n < len P holds
( ( P . (n + 1) DJoins P . n,P . (n + 2),G implies IT1 . (P . (n + 1)) = (EL . (P . (n + 1))) + (P .tolerance EL) ) & ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies IT1 . (P . (n + 1)) = (EL . (P . (n + 1))) - (P .tolerance EL) ) ) ) & ( for e being set st e in the_Edges_of G & not e in P .edges() holds
IT2 . e = EL . e ) & ( for n being odd Nat st n < len P holds
( ( P . (n + 1) DJoins P . n,P . (n + 2),G implies IT2 . (P . (n + 1)) = (EL . (P . (n + 1))) + (P .tolerance EL) ) & ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies IT2 . (P . (n + 1)) = (EL . (P . (n + 1))) - (P .tolerance EL) ) ) ) implies IT1 = IT2 )
assume that
A35: for e being set st e in the_Edges_of G & not e in P .edges() holds
IT1 . e = EL . e and
A36: for n being odd Nat st n < len P holds
( ( P . (n + 1) DJoins P . n,P . (n + 2),G implies IT1 . (P . (n + 1)) = (EL . (P . (n + 1))) + (P .tolerance EL) ) & ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies IT1 . (P . (n + 1)) = (EL . (P . (n + 1))) - (P .tolerance EL) ) ) and
A37: for e being set st e in the_Edges_of G & not e in P .edges() holds
IT2 . e = EL . e and
A38: for n being odd Nat st n < len P holds
( ( P . (n + 1) DJoins P . n,P . (n + 2),G implies IT2 . (P . (n + 1)) = (EL . (P . (n + 1))) + (P .tolerance EL) ) & ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies IT2 . (P . (n + 1)) = (EL . (P . (n + 1))) - (P .tolerance EL) ) ) ; :: thesis: IT1 = IT2

now :: thesis: for e being object st e in the_Edges_of G holds
IT1 . e = IT2 . e

let e be object ; :: thesis: ( e in the_Edges_of G implies IT1 . e = IT2 . e )
assume A39: e in the_Edges_of G ; :: thesis: IT1 . e = IT2 . e

now :: thesis: IT1 . e = IT2 . e

per cases ( not e in P .edges() or e in P .edges() ) ;

suppose A40: not e in P .edges() ; :: thesis: IT1 . e = IT2 . e

then IT1 . e = EL . e by A35, A39;
hence IT1 . e = IT2 . e by A37, A39, A40; :: thesis: verum

end;

suppose e in P .edges() ; :: thesis: IT1 . e = IT2 . e

then consider n being odd Element of NAT such that
A41: n < len P and
A42: P . (n + 1) = e by GLIB_001:100;

now :: thesis: IT1 . e = IT2 . e

per cases ( P . (n + 1) DJoins P . n,P . (n + 2),G or not P . (n + 1) DJoins P . n,P . (n + 2),G ) ;

suppose A43: P . (n + 1) DJoins P . n,P . (n + 2),G ; :: thesis: IT1 . e = IT2 . e

then IT1 . e = (EL . (P . (n + 1))) + (P .tolerance EL) by A36, A41, A42;
hence IT1 . e = IT2 . e by A38, A41, A42, A43; :: thesis: verum

end;

suppose A44: not P . (n + 1) DJoins P . n,P . (n + 2),G ; :: thesis: IT1 . e = IT2 . e

then IT1 . e = (EL . (P . (n + 1))) - (P .tolerance EL) by A36, A41, A42;
hence IT1 . e = IT2 . e by A38, A41, A42, A44; :: thesis: verum

end;

end;

end;

hence IT1 . e = IT2 . e ; :: thesis: verum

end;

end;

end;

hence IT1 . e = IT2 . e ; :: thesis: verum

end;

hence IT1 = IT2 by PBOOLE:3; :: thesis: verum