defpred S1[ object , object ] means ( ( $1 in the_Edges_of G & not $1 in P .edges() implies $2 = EL . $1 ) & ( for n being odd Element of NAT st n < len P & $1 = P . (n + 1) holds
( ( P . (n + 1) DJoins P . n,P . (n + 2),G implies $2 = (EL . (P . (n + 1))) + (P .tolerance EL) ) & ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies $2 = (EL . (P . (n + 1))) - (P .tolerance EL) ) ) ) );
now :: thesis: for x being object st x in the_Edges_of G holds
ex y being object st S1[x,y]
let x be object ; :: thesis: ( x in the_Edges_of G implies ex y being object st S1[x,y] )
assume x in the_Edges_of G ; :: thesis: ex y being object st S1[x,y]
now :: thesis: ex y being set st S1[x,y]
per cases ( not x in P .edges() or x in P .edges() ) ;
suppose A2: not x in P .edges() ; :: thesis: ex y being set st S1[x,y]
set y = EL . x;
for n being odd Element of NAT st n < len P & x = P . (n + 1) holds
( ( P . (n + 1) DJoins P . n,P . (n + 2),G implies EL . x = (EL . (P . (n + 1))) + (P .tolerance EL) ) & ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies EL . x = (EL . (P . (n + 1))) - (P .tolerance EL) ) ) by A2, GLIB_001:100;
hence ex y being set st S1[x,y] ; :: thesis: verum
end;
suppose A3: x in P .edges() ; :: thesis: ex y being set st S1[x,y]
then consider n being odd Element of NAT such that
A4: n < len P and
A5: P . (n + 1) = x by GLIB_001:100;
A6: 1 <= n + 1 by NAT_1:11;
A7: n + 1 <= len P by A4, NAT_1:13;
now :: thesis: ex y being set st S1[x,y]
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 A8: P . (n + 1) DJoins P . n,P . (n + 2),G ; :: thesis: ex y being set st S1[x,y]
set y = (EL . (P . (n + 1))) + (P .tolerance EL);
now :: thesis: ( ( x in the_Edges_of G & not x in P .edges() implies (EL . (P . (n + 1))) + (P .tolerance EL) = EL . x ) & ( for m being odd Element of NAT st m < len P & P . (m + 1) = x holds
( ( P . (m + 1) DJoins P . m,P . (m + 2),G implies (EL . (P . (n + 1))) + (P .tolerance EL) = (EL . (P . (n + 1))) + (P .tolerance EL) ) & ( not P . (m + 1) DJoins P . m,P . (m + 2),G implies (EL . (P . (n + 1))) + (P .tolerance EL) = (EL . (P . (m + 1))) - (P .tolerance EL) ) ) ) )
thus ( x in the_Edges_of G & not x in P .edges() implies (EL . (P . (n + 1))) + (P .tolerance EL) = EL . x ) by A3; :: thesis: for m being odd Element of NAT st m < len P & P . (m + 1) = x holds
( ( P . (m + 1) DJoins P . m,P . (m + 2),G implies (EL . (P . (n + 1))) + (P .tolerance EL) = (EL . (P . (n + 1))) + (P .tolerance EL) ) & ( not P . (m + 1) DJoins P . m,P . (m + 2),G implies (EL . (P . (n + 1))) + (P .tolerance EL) = (EL . (P . (m + 1))) - (P .tolerance EL) ) )
let m be odd Element of NAT ; :: thesis: ( m < len P & P . (m + 1) = x implies ( ( P . (m + 1) DJoins P . m,P . (m + 2),G implies (EL . (P . (n + 1))) + (P .tolerance EL) = (EL . (P . (n + 1))) + (P .tolerance EL) ) & ( not P . (m + 1) DJoins P . m,P . (m + 2),G implies (EL . (P . (n + 1))) + (P .tolerance EL) = (EL . (P . (m + 1))) - (P .tolerance EL) ) ) )
assume that
A9: m < len P and
A10: P . (m + 1) = x ; :: thesis: ( ( P . (m + 1) DJoins P . m,P . (m + 2),G implies (EL . (P . (n + 1))) + (P .tolerance EL) = (EL . (P . (n + 1))) + (P .tolerance EL) ) & ( not P . (m + 1) DJoins P . m,P . (m + 2),G implies (EL . (P . (n + 1))) + (P .tolerance EL) = (EL . (P . (m + 1))) - (P .tolerance EL) ) )
1 <= m + 1 by NAT_1:11;
then A11: n + 1 <= m + 1 by A5, A7, A10, GLIB_001:138;
thus ( P . (m + 1) DJoins P . m,P . (m + 2),G implies (EL . (P . (n + 1))) + (P .tolerance EL) = (EL . (P . (n + 1))) + (P .tolerance EL) ) ; :: thesis: ( not P . (m + 1) DJoins P . m,P . (m + 2),G implies (EL . (P . (n + 1))) + (P .tolerance EL) = (EL . (P . (m + 1))) - (P .tolerance EL) )
assume A12: not P . (m + 1) DJoins P . m,P . (m + 2),G ; :: thesis: (EL . (P . (n + 1))) + (P .tolerance EL) = (EL . (P . (m + 1))) - (P .tolerance EL)
m + 1 <= len P by A9, NAT_1:13;
then m + 1 <= n + 1 by A5, A6, A10, GLIB_001:138;
then m + 1 = n + 1 by A11, XXREAL_0:1;
hence (EL . (P . (n + 1))) + (P .tolerance EL) = (EL . (P . (m + 1))) - (P .tolerance EL) by A8, A12; :: thesis: verum
end;
then S1[x,(EL . (P . (n + 1))) + (P .tolerance EL)] by A5;
hence ex y being set st S1[x,y] ; :: thesis: verum
end;
suppose A13: not P . (n + 1) DJoins P . n,P . (n + 2),G ; :: thesis: ex y being set st S1[x,y]
set y = (EL . (P . (n + 1))) - (P .tolerance EL);
now :: thesis: ( ( x in the_Edges_of G & not x in P .edges() implies (EL . (P . (n + 1))) - (P .tolerance EL) = EL . x ) & ( for m being odd Element of NAT st m < len P & P . (m + 1) = x holds
( ( P . (m + 1) DJoins P . m,P . (m + 2),G implies (EL . (P . (n + 1))) - (P .tolerance EL) = (EL . (P . (n + 1))) + (P .tolerance EL) ) & ( not P . (m + 1) DJoins P . m,P . (m + 2),G implies (EL . (P . (n + 1))) - (P .tolerance EL) = (EL . (P . (n + 1))) - (P .tolerance EL) ) ) ) )
thus ( x in the_Edges_of G & not x in P .edges() implies (EL . (P . (n + 1))) - (P .tolerance EL) = EL . x ) by A3; :: thesis: for m being odd Element of NAT st m < len P & P . (m + 1) = x holds
( ( P . (m + 1) DJoins P . m,P . (m + 2),G implies (EL . (P . (n + 1))) - (P .tolerance EL) = (EL . (P . (n + 1))) + (P .tolerance EL) ) & ( not P . (m + 1) DJoins P . m,P . (m + 2),G implies (EL . (P . (n + 1))) - (P .tolerance EL) = (EL . (P . (n + 1))) - (P .tolerance EL) ) )
let m be odd Element of NAT ; :: thesis: ( m < len P & P . (m + 1) = x implies ( ( P . (m + 1) DJoins P . m,P . (m + 2),G implies (EL . (P . (n + 1))) - (P .tolerance EL) = (EL . (P . (n + 1))) + (P .tolerance EL) ) & ( not P . (m + 1) DJoins P . m,P . (m + 2),G implies (EL . (P . (n + 1))) - (P .tolerance EL) = (EL . (P . (n + 1))) - (P .tolerance EL) ) ) )
assume that
A14: m < len P and
A15: P . (m + 1) = x ; :: thesis: ( ( P . (m + 1) DJoins P . m,P . (m + 2),G implies (EL . (P . (n + 1))) - (P .tolerance EL) = (EL . (P . (n + 1))) + (P .tolerance EL) ) & ( not P . (m + 1) DJoins P . m,P . (m + 2),G implies (EL . (P . (n + 1))) - (P .tolerance EL) = (EL . (P . (n + 1))) - (P .tolerance EL) ) )
1 <= m + 1 by NAT_1:11;
then A16: n + 1 <= m + 1 by A5, A7, A15, GLIB_001:138;
m + 1 <= len P by A14, NAT_1:13;
then m + 1 <= n + 1 by A5, A6, A15, GLIB_001:138;
then m + 1 = n + 1 by A16, XXREAL_0:1;
hence ( P . (m + 1) DJoins P . m,P . (m + 2),G implies (EL . (P . (n + 1))) - (P .tolerance EL) = (EL . (P . (n + 1))) + (P .tolerance EL) ) by A13; :: thesis: ( not P . (m + 1) DJoins P . m,P . (m + 2),G implies (EL . (P . (n + 1))) - (P .tolerance EL) = (EL . (P . (n + 1))) - (P .tolerance EL) )
assume not P . (m + 1) DJoins P . m,P . (m + 2),G ; :: thesis: (EL . (P . (n + 1))) - (P .tolerance EL) = (EL . (P . (n + 1))) - (P .tolerance EL)
thus (EL . (P . (n + 1))) - (P .tolerance EL) = (EL . (P . (n + 1))) - (P .tolerance EL) ; :: thesis: verum
end;
then S1[x,(EL . (P . (n + 1))) - (P .tolerance EL)] by A5;
hence ex y being set st S1[x,y] ; :: thesis: verum
end;
end;
end;
hence ex y being set st S1[x,y] ; :: thesis: verum
end;
end;
end;
hence ex y being object st S1[x,y] ; :: thesis: verum
end;
then A17: for x being object st x in the_Edges_of G holds
ex y being object st S1[x,y] ;
consider IT being Function such that
A18: dom IT = the_Edges_of G and
A19: for e being object st e in the_Edges_of G holds
S1[e,IT . e] from CLASSES1:sch 1(A17);
 rng IT c= NAT
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng IT or y in NAT )
assume y in rng IT ; :: thesis: y in NAT
then consider e being object such that
A20: e in dom IT and
A21: IT . e = y by FUNCT_1:def 3;
now :: thesis: y in NAT
per cases ( not e in P .edges() or e in P .edges() ) ;
suppose A22: e in P .edges() ; :: thesis: y in NAT
then consider n being odd Element of NAT such that
A23: n < len P and
A24: P . (n + 1) = e by GLIB_001:100;
A25: P is V5() by A22, GLIB_001:136;
now :: thesis: y in NAT
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 P . (n + 1) DJoins P . n,P . (n + 2),G ; :: thesis: y in NAT
then y = (EL . (P . (n + 1))) + (P .tolerance EL) by A19, A21, A23, A24;
hence y in NAT by ORDINAL1:def 12; :: thesis: verum
end;
suppose A26: not P . (n + 1) DJoins P . n,P . (n + 2),G ; :: thesis: y in NAT
set n1div2 = (n + 1) div 2;
A27: 1 <= n + 1 by NAT_1:11;
n + 1 <= len P by A23, NAT_1:13;
then (n + 1) div 2 in dom (P .edgeSeq()) by A27, GLIB_001:77;
then A28: (n + 1) div 2 in dom (P .flowSeq EL) by A1, Def15;
2 divides n + 1 by PEPIN:22;
then A29: 2 * ((n + 1) div 2) = n + 1 by NAT_D:3;
then A30: (2 * ((n + 1) div 2)) + 1 = n + (1 + 1) ;
(2 * ((n + 1) div 2)) - 1 = n by A29;
then (P .flowSeq EL) . ((n + 1) div 2) = EL . e by A1, A24, A26, A28, A30, Def15;
then EL . e in rng (P .flowSeq EL) by A28, FUNCT_1:def 3;
then A31: P .tolerance EL <= EL . e by A1, A25, Def16;
y = (EL . e) - (P .tolerance EL) by A18, A19, A20, A21, A23, A24, A26;
hence y in NAT by A31, INT_1:5; :: thesis: verum
end;
end;
end;
hence y in NAT ; :: thesis: verum
end;
end;
end;
hence y in NAT ; :: thesis: verum
end;
then reconsider IT = IT as natural-valued ManySortedSet of the_Edges_of G by A18, PARTFUN1:def 2, RELAT_1:def 18, VALUED_0:def 6;
take IT ; :: thesis: ( ( for e being set st e in the_Edges_of G & not e in P .edges() holds
IT . e = EL . e ) & ( for n being odd Nat st n < len P holds
( ( P . (n + 1) DJoins P . n,P . (n + 2),G implies IT . (P . (n + 1)) = (EL . (P . (n + 1))) + (P .tolerance EL) ) & ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies IT . (P . (n + 1)) = (EL . (P . (n + 1))) - (P .tolerance EL) ) ) ) )
thus for e being set st e in the_Edges_of G & not e in P .edges() holds
IT . e = EL . e by A19; :: thesis: for n being odd Nat st n < len P holds
( ( P . (n + 1) DJoins P . n,P . (n + 2),G implies IT . (P . (n + 1)) = (EL . (P . (n + 1))) + (P .tolerance EL) ) & ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies IT . (P . (n + 1)) = (EL . (P . (n + 1))) - (P .tolerance EL) ) )
let n be odd Nat; :: thesis: ( n < len P implies ( ( P . (n + 1) DJoins P . n,P . (n + 2),G implies IT . (P . (n + 1)) = (EL . (P . (n + 1))) + (P .tolerance EL) ) & ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies IT . (P . (n + 1)) = (EL . (P . (n + 1))) - (P .tolerance EL) ) ) )
reconsider n9 = n as odd Element of NAT by ORDINAL1:def 12;
A32: n9 = n ;
assume A33: n < len P ; :: thesis: ( ( P . (n + 1) DJoins P . n,P . (n + 2),G implies IT . (P . (n + 1)) = (EL . (P . (n + 1))) + (P .tolerance EL) ) & ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies IT . (P . (n + 1)) = (EL . (P . (n + 1))) - (P .tolerance EL) ) )
then P . (n + 1) Joins P . n,P . (n9 + 2),G by GLIB_001:def 3;
then A34: P . (n + 1) in the_Edges_of G ;
thus ( P . (n + 1) DJoins P . n,P . (n + 2),G implies IT . (P . (n + 1)) = (EL . (P . (n + 1))) + (P .tolerance EL) ) by A19, A32, A33; :: thesis: ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies IT . (P . (n + 1)) = (EL . (P . (n + 1))) - (P .tolerance EL) )
assume not P . (n + 1) DJoins P . n,P . (n + 2),G ; :: thesis: IT . (P . (n + 1)) = (EL . (P . (n + 1))) - (P .tolerance EL)
hence IT . (P . (n + 1)) = (EL . (P . (n + 1))) - (P .tolerance EL) by A19, A32, A33, A34; :: thesis: verum