defpred S₁[ 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 :: thesis: for n, x being set ex y being set st S₁[n,x,y]

let n, x be set ; :: thesis: ex y being set st S₁[n,x,y]

now :: thesis: ex y being set st S₁[n,x,y]

per cases ( x is AP:VLabeling of EL or not x is AP:VLabeling of EL ) ;

suppose x is AP:VLabeling of EL ; :: thesis: ex y being set st S₁[n,x,y]

then reconsider Gn = x as AP:VLabeling of EL ;
S₁[n,x, AP:Step Gn] ;
hence ex y being set st S₁[n,x,y] ; :: thesis: verum

end;

suppose x is not AP:VLabeling of EL ; :: thesis: ex y being set st S₁[n,x,y]

hence ex y being set st S₁[n,x,y] ; :: thesis: verum

end;

end;

end;

hence ex y being set st S₁[n,x,y] ; :: thesis: verum

end;

then A2: for n being Nat
for x being set ex y being set st S₁[n,x,y] ;
consider IT being Function such that
A3: ( dom IT = NAT & IT . 0 = source .--> 1 & ( for n being Nat holds S₁[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 S₂[ Nat] means IT . $1 is AP:VLabeling of EL;

A4: now :: thesis: for n being Nat st S₂[n] holds
S₂[n + 1]

let n be Nat; :: thesis: ( S₂[n] implies S₂[n + 1] )
assume A5: S₂[n] ; :: thesis: S₂[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 S₂[n + 1] ; :: thesis: 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: S₂[ 0 ] by A3, Def5;
for n being Nat holds S₂[n] from NAT_1:sch 2(A6, A4);
then reconsider IT = IT as AP:VLabelingSeq of EL by Def11;
take IT ; :: thesis: ( IT . 0 = source .--> 1 & ( for n being Nat holds IT . (n + 1) = AP:Step (IT . n) ) )
thus IT . 0 = source .--> 1 by A3; :: thesis: for n being Nat holds IT . (n + 1) = AP:Step (IT . n)
let n be Nat; :: thesis: 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) ; :: thesis: verum