defpred S_{1}[ set , set , set ] means ( ( $2 is MCS:Labeling of G & $1 is Nat & ex nn being Nat ex Gn, Gn1 being MCS:Labeling of G st

( $1 = nn & $2 = Gn & $3 = Gn1 & Gn1 = MCS:Step Gn ) ) or ( ( not $2 is MCS:Labeling of G or not $1 is Nat ) & $2 = $3 ) );

for x being set ex y being set st S_{1}[n,x,y]
;

consider IT being Function such that

A3: ( dom IT = NAT & IT . 0 = MCS:Init G & ( for n being Nat holds S_{1}[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_{2}[ Nat] means IT . $1 is MCS:Labeling of G;

_{2}[ 0 ]
by A3;

for n being Nat holds S_{2}[n]
from NAT_1:sch 2(A6, A4);

then reconsider IT = IT as MCS:LabelingSeq of G by Def23;

take IT ; :: thesis: ( IT . 0 = MCS:Init G & ( for n being Nat holds IT . (n + 1) = MCS:Step (IT . n) ) )

thus IT . 0 = MCS:Init G by A3; :: thesis: for n being Nat holds IT . (n + 1) = MCS:Step (IT . n)

let n be Nat; :: thesis: IT . (n + 1) = MCS:Step (IT . n)

ex nn being Nat ex Gn, Gn1 being MCS:Labeling of G st

( n = nn & IT . n = Gn & IT . (n + 1) = Gn1 & Gn1 = MCS:Step Gn ) by A3;

hence IT . (n + 1) = MCS:Step (IT . n) ; :: thesis: verum

( $1 = nn & $2 = Gn & $3 = Gn1 & Gn1 = MCS:Step Gn ) ) or ( ( not $2 is MCS:Labeling of G or not $1 is Nat ) & $2 = $3 ) );

now :: thesis: for n, x being set ex y being set st S_{1}[n,x,y]

then A2:
for n being Natlet n, x be set ; :: thesis: ex y being set st S_{1}[n,x,y]

_{1}[n,x,y]
; :: thesis: verum

end;now :: thesis: ex y being set st S_{1}[n,x,y]end;

hence
ex y being set st Sper cases
( ( x is MCS:Labeling of G & n is Nat ) or not x is MCS:Labeling of G or not n is Nat )
;

end;

suppose A1:
( x is MCS:Labeling of G & n is Nat )
; :: thesis: ex y being set st S_{1}[n,x,y]

then reconsider Gn = x as MCS:Labeling of G ;

ex SGn being MCS:Labeling of G st SGn = MCS:Step Gn ;

hence ex y being set st S_{1}[n,x,y]
by A1; :: thesis: verum

end;ex SGn being MCS:Labeling of G st SGn = MCS:Step Gn ;

hence ex y being set st S

suppose
( not x is MCS:Labeling of G or not n is Nat )
; :: thesis: ex y being set st S_{1}[n,x,y]

end;

end;

for x being set ex y being set st S

consider IT being Function such that

A3: ( dom IT = NAT & IT . 0 = MCS:Init G & ( for n being Nat holds S

reconsider IT = IT as ManySortedSet of NAT by A3, PARTFUN1:def 2, RELAT_1:def 18;

defpred S

A4: now :: thesis: for n being Nat st S_{2}[n] holds

S_{2}[n + 1]

A6:
SS

let n be Nat; :: thesis: ( S_{2}[n] implies S_{2}[n + 1] )

assume A5: S_{2}[n]
; :: thesis: S_{2}[n + 1]

ex nn being Nat ex Gn, Gn1 being MCS:Labeling of G st

( n = nn & IT . n = Gn & IT . (n + 1) = Gn1 & Gn1 = MCS:Step Gn ) by A3, A5;

hence S_{2}[n + 1]
; :: thesis: verum

end;assume A5: S

ex nn being Nat ex Gn, Gn1 being MCS:Labeling of G st

( n = nn & IT . n = Gn & IT . (n + 1) = Gn1 & Gn1 = MCS:Step Gn ) by A3, A5;

hence S

for n being Nat holds S

then reconsider IT = IT as MCS:LabelingSeq of G by Def23;

take IT ; :: thesis: ( IT . 0 = MCS:Init G & ( for n being Nat holds IT . (n + 1) = MCS:Step (IT . n) ) )

thus IT . 0 = MCS:Init G by A3; :: thesis: for n being Nat holds IT . (n + 1) = MCS:Step (IT . n)

let n be Nat; :: thesis: IT . (n + 1) = MCS:Step (IT . n)

ex nn being Nat ex Gn, Gn1 being MCS:Labeling of G st

( n = nn & IT . n = Gn & IT . (n + 1) = Gn1 & Gn1 = MCS:Step Gn ) by A3;

hence IT . (n + 1) = MCS:Step (IT . n) ; :: thesis: verum