defpred S₁[ set , set , set ] means ( ( $2 is PRIM:Labeling of G & ex Gn, Gn1 being PRIM:Labeling of G st
( $2 = Gn & $3 = Gn1 & Gn1 = PRIM:Step Gn ) ) or ( $2 is not PRIM:Labeling of G & $2 = $3 ) );

now

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

now

per cases ( x is PRIM:Labeling of G or not x is PRIM:Labeling of G ) ;

suppose x is PRIM:Labeling of G ; :: thesis: ex y being set st S₁[n,x,y]

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

end;

suppose x is not PRIM:Labeling of G ; :: 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 A1: for n being Element of 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 = PRIM:Init G & ( for n being Element of NAT holds S₁[n,IT . n,IT . (n + 1)] ) ) from RECDEF_1:sch 1(A1);
reconsider IT = IT as ManySortedSet of by A3, PARTFUN1:def 4, RELAT_1:def 18;
defpred S₂[ Nat] means IT . $1 is PRIM:Labeling of G;
A4: S₂[ 0 ] by A3;

A5: now

let n be Nat; :: thesis: ( S₂[n] implies S₂[n + 1] )
reconsider n' = n as Element of NAT by ORDINAL1:def 13;
assume S₂[n] ; :: thesis: S₂[n + 1]
then consider Gn, Gn1 being PRIM:Labeling of G such that
A7: ( IT . n' = Gn & IT . (n + 1) = Gn1 & Gn1 = PRIM:Step Gn ) by A3;
thus S₂[n + 1] by A7; :: thesis: verum

end;

for n being Nat holds S₂[n] from NAT_1:sch 2(A4, A5);
then reconsider IT = IT as PRIM:LabelingSeq of G by dPRIMSeq;
take IT ; :: thesis: ( IT . 0 = PRIM:Init G & ( for n being Nat holds IT . (n + 1) = PRIM:Step (IT . n) ) )
thus IT . 0 = PRIM:Init G by A3; :: thesis: for n being Nat holds IT . (n + 1) = PRIM:Step (IT . n)
let n be Nat; :: thesis: IT . (n + 1) = PRIM:Step (IT . n)
reconsider n' = n as Element of NAT by ORDINAL1:def 13;
consider Gn, Gn1 being PRIM:Labeling of G such that
A9: ( IT . n' = Gn & IT . (n + 1) = Gn1 & Gn1 = PRIM:Step Gn ) by A3;
thus IT . (n + 1) = PRIM:Step (IT . n) by A9; :: thesis: verum