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 for x being object st x in the_Edges_of G holds
ex y being object st S1[x,y]let x be
object ;
( x in the_Edges_of G implies ex y being object st S1[x,y] )assume
x in the_Edges_of G
;
ex y being object st S1[x,y]now ex y being set st S1[x,y]per cases
( not x in P .edges() or x in P .edges() )
;
suppose A3:
x in P .edges()
;
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 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
;
ex y being set st S1[x,y]set y =
(EL . (P . (n + 1))) + (P .tolerance EL);
now ( ( 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;
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 ;
( 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
;
( ( 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) )
;
( 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
;
(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;
verum end; then
S1[
x,
(EL . (P . (n + 1))) + (P .tolerance EL)]
by A5;
hence
ex
y being
set st
S1[
x,
y]
;
verum end; suppose A13:
not
P . (n + 1) DJoins P . n,
P . (n + 2),
G
;
ex y being set st S1[x,y]set y =
(EL . (P . (n + 1))) - (P .tolerance EL);
now ( ( 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;
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 ;
( 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
;
( ( 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;
( 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
;
(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)
;
verum end; then
S1[
x,
(EL . (P . (n + 1))) - (P .tolerance EL)]
by A5;
hence
ex
y being
set st
S1[
x,
y]
;
verum end; end; end; hence
ex
y being
set st
S1[
x,
y]
;
verum end; end; end; hence
ex
y being
object st
S1[
x,
y]
;
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 ;
TARSKI:def 3 ( not y in rng IT or y in NAT )
assume
y in rng IT
;
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 y in NAT per cases
( not e in P .edges() or e in P .edges() )
;
suppose A22:
e in P .edges()
;
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 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 A26:
not
P . (n + 1) DJoins P . n,
P . (n + 2),
G
;
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;
verum end; end; end; hence
y in NAT
;
verum end; end; end;
hence
y in NAT
;
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
; ( ( 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; 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; ( 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
; ( ( 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; ( 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
; 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; verum