defpred S1[ set , set , set ] means ( ( $2 is AP:VLabeling of EL & ex Gn, Gn1 being AP:VLabeling of EL st
( $2 = Gn & $3 = Gn1 & Gn1 = AP:Step Gn ) ) or ( $2 is not AP:VLabeling of EL & $2 = $3 ) );
A1:
rng (source .--> 1) = {1}
by FUNCOP_1:8;
now for n, x being set ex y being set st S1[n,x,y]let n,
x be
set ;
ex y being set st S1[n,x,y]now ex y being set st S1[n,x,y]end; hence
ex
y being
set st
S1[
n,
x,
y]
;
verum end;
then A2:
for n being Nat
for x being set ex y being set st S1[n,x,y]
;
consider IT being Function such that
A3:
( dom IT = NAT & IT . 0 = source .--> 1 & ( for n being Nat holds S1[n,IT . n,IT . (n + 1)] ) )
from RECDEF_1:sch 1(A2);
reconsider IT = IT as ManySortedSet of NAT by A3, PARTFUN1:def 2, RELAT_1:def 18;
defpred S2[ Nat] means IT . $1 is AP:VLabeling of EL;
A4:
now for n being Nat st S2[n] holds
S2[n + 1]let n be
Nat;
( S2[n] implies S2[n + 1] )assume A5:
S2[
n]
;
S2[n + 1]
ex
Gn,
Gn1 being
AP:VLabeling of
EL st
(
IT . n = Gn &
IT . (n + 1) = Gn1 &
Gn1 = AP:Step Gn )
by A3, A5;
hence
S2[
n + 1]
;
verum end;
dom (source .--> 1) = {source}
;
then
source .--> 1 is Relation of (the_Vertices_of G),({1} \/ (the_Edges_of G))
by A1, RELSET_1:4, XBOOLE_1:7;
then A6:
S2[ 0 ]
by A3, Def5;
for n being Nat holds S2[n]
from NAT_1:sch 2(A6, A4);
then reconsider IT = IT as AP:VLabelingSeq of EL by Def11;
take
IT
; ( IT . 0 = source .--> 1 & ( for n being Nat holds IT . (n + 1) = AP:Step (IT . n) ) )
thus
IT . 0 = source .--> 1
by A3; for n being Nat holds IT . (n + 1) = AP:Step (IT . n)
let n be Nat; IT . (n + 1) = AP:Step (IT . n)
ex Gn, Gn1 being AP:VLabeling of EL st
( IT . n = Gn & IT . (n + 1) = Gn1 & Gn1 = AP:Step Gn )
by A3;
hence
IT . (n + 1) = AP:Step (IT . n)
; verum