let G be finite real-weighted WGraph; :: thesis: ( PRIM:CompSeq G is halting & ((PRIM:CompSeq G) .Lifespan() ) + 1 = card (G .reachableFrom (choose (the_Vertices_of G))) )
set PCS = PRIM:CompSeq G;
set src = choose (the_Vertices_of G);
set RFS = G .reachableFrom (choose (the_Vertices_of G));
consider n being Nat such that
A1: n + 1 = card (G .reachableFrom (choose (the_Vertices_of G))) by NAT_1:6;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
set Gn = (PRIM:CompSeq G) . n;
set Gn1 = (PRIM:CompSeq G) . (n + 1);
A2: card (G .reachableFrom (choose (the_Vertices_of G))) <= (card (G .reachableFrom (choose (the_Vertices_of G)))) + 1 by NAT_1:11;
A3: card (((PRIM:CompSeq G) . (n + 1)) `1 ) = min ((card (G .reachableFrom (choose (the_Vertices_of G)))) + 1),(card (G .reachableFrom (choose (the_Vertices_of G)))) by A1, Th36
.= card (G .reachableFrom (choose (the_Vertices_of G))) by A2, XXREAL_0:def 9 ;
set e = choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n));
A4: card (((PRIM:CompSeq G) . n) `1 ) = min (card (G .reachableFrom (choose (the_Vertices_of G)))),(card (G .reachableFrom (choose (the_Vertices_of G)))) by A1, Th36
.= card (G .reachableFrom (choose (the_Vertices_of G))) ;
A5: (PRIM:CompSeq G) . (n + 1) = PRIM:Step ((PRIM:CompSeq G) . n) by Def17;
then A6: ((PRIM:CompSeq G) . n) `1 c= ((PRIM:CompSeq G) . (n + 1)) `1 by Th29;

A7: now

assume ((PRIM:CompSeq G) . n) `1 <> ((PRIM:CompSeq G) . (n + 1)) `1 ; :: thesis: contradiction
then ((PRIM:CompSeq G) . n) `1 c< ((PRIM:CompSeq G) . (n + 1)) `1 by A6, XBOOLE_0:def 8;
hence contradiction by A4, A3, CARD_2:67; :: thesis: verum

end;

now

assume PRIM:NextBestEdges ((PRIM:CompSeq G) . n) <> {} ; :: thesis: contradiction
then consider v being Vertex of G such that
A8: not v in ((PRIM:CompSeq G) . n) `1 and
A9: (PRIM:CompSeq G) . (n + 1) = [((((PRIM:CompSeq G) . n) `1 ) \/ {v}),((((PRIM:CompSeq G) . n) `2 ) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n)))})] by A5, Th28;
A10: v in {v} by TARSKI:def 1;
((PRIM:CompSeq G) . (n + 1)) `1 = (((PRIM:CompSeq G) . n) `1 ) \/ {v} by A9, MCART_1:7;
hence contradiction by A7, A8, A10, XBOOLE_0:def 3; :: thesis: verum

end;

then A11: (PRIM:CompSeq G) . (n + 1) = (PRIM:CompSeq G) . n by A5, Def15;
hence A12: PRIM:CompSeq G is halting by GLIB_000:def 56; :: thesis: ((PRIM:CompSeq G) .Lifespan() ) + 1 = card (G .reachableFrom (choose (the_Vertices_of G)))

now

let m be Nat; :: thesis: ( (PRIM:CompSeq G) . m = (PRIM:CompSeq G) . (m + 1) implies n <= m )
set Gm = (PRIM:CompSeq G) . m;
assume A13: (PRIM:CompSeq G) . m = (PRIM:CompSeq G) . (m + 1) ; :: thesis: n <= m

now

assume m < n ; :: thesis: contradiction
then A14: m + 1 <= n by NAT_1:13;
n + 0 < card (G .reachableFrom (choose (the_Vertices_of G))) by A1, XREAL_1:10;
then A15: m + 1 < card (G .reachableFrom (choose (the_Vertices_of G))) by A14, XXREAL_0:2;
then A16: (m + 1) + 1 <= card (G .reachableFrom (choose (the_Vertices_of G))) by NAT_1:13;
A17: card (((PRIM:CompSeq G) . m) `1 ) = min (m + 1),(card (G .reachableFrom (choose (the_Vertices_of G)))) by Th36
.= m + 1 by A15, XXREAL_0:def 9 ;
card (((PRIM:CompSeq G) . m) `1 ) = min ((m + 1) + 1),(card (G .reachableFrom (choose (the_Vertices_of G)))) by A13, Th36
.= (m + 1) + 1 by A16, XXREAL_0:def 9 ;
hence contradiction by A17; :: thesis: verum

end;

hence n <= m ; :: thesis: verum

end;

hence ((PRIM:CompSeq G) .Lifespan() ) + 1 = card (G .reachableFrom (choose (the_Vertices_of G))) by A1, A11, A12, GLIB_000:def 57; :: thesis: verum