let IT1, IT2 be FF:ELabelingSeq of G; ( IT1 . 0 = (the_Edges_of G) --> 0 & ( for n being Nat holds IT1 . (n + 1) = FF:Step ((IT1 . n),source,sink) ) & IT2 . 0 = (the_Edges_of G) --> 0 & ( for n being Nat holds IT2 . (n + 1) = FF:Step ((IT2 . n),source,sink) ) implies IT1 = IT2 )
assume that
A8:
IT1 . 0 = (the_Edges_of G) --> 0
and
A9:
for n being Nat holds IT1 . (n + 1) = FF:Step ((IT1 . n),source,sink)
and
A10:
IT2 . 0 = (the_Edges_of G) --> 0
and
A11:
for n being Nat holds IT2 . (n + 1) = FF:Step ((IT2 . n),source,sink)
; IT1 = IT2
defpred S1[ Nat] means IT1 . $1 = IT2 . $1;
A12:
now for n being Nat st S1[n] holds
S1[n + 1]let n be
Nat;
( S1[n] implies S1[n + 1] )assume A13:
S1[
n]
;
S1[n + 1]
IT2 . (n + 1) = FF:Step (
(IT2 . n),
source,
sink)
by A11;
hence
S1[
n + 1]
by A9, A13;
verum end;
A14:
S1[ 0 ]
by A8, A10;
for n being Nat holds S1[n]
from NAT_1:sch 2(A14, A12);
then
for n being object st n in NAT holds
IT1 . n = IT2 . n
;
hence
IT1 = IT2
by PBOOLE:3; verum