let G be _finite real-weighted WGraph; :: thesis: for n being Nat holds card (((PRIM:CompSeq G) . n) `1) = min ((n + 1),(card (G .reachableFrom the Element of the_Vertices_of G)))
set CS = PRIM:CompSeq G;
set src = the Element of the_Vertices_of G;
defpred S<sub>1</sub>[ Nat] means card (((PRIM:CompSeq G) . $1) `1) = min (($1 + 1),(card (G .reachableFrom the Element of the_Vertices_of G)));
set G0 = (PRIM:CompSeq G) . 0;
the Element of the_Vertices_of G in G .reachableFrom the Element of the_Vertices_of G by GLIB_002:9;
then { the Element of the_Vertices_of G} c= G .reachableFrom the Element of the_Vertices_of G by ZFMISC_1:31;
then card { the Element of the_Vertices_of G} <= card (G .reachableFrom the Element of the_Vertices_of G) by NAT_1:43;
then A1: 0 + 1 <= card (G .reachableFrom the Element of the_Vertices_of G) by CARD_1:30;

A2: 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 A3: S₁[n] ; :: thesis: S₁[n + 1]
set Gn = (PRIM:CompSeq G) . n;
set Gn1 = (PRIM:CompSeq G) . (n + 1);
set e = the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n);
A4: (PRIM:CompSeq G) . (n + 1) = PRIM:Step ((PRIM:CompSeq G) . n) by Def17;

now :: thesis: S₁[n + 1]

per cases ( PRIM:NextBestEdges ((PRIM:CompSeq G) . n) = {} or PRIM:NextBestEdges ((PRIM:CompSeq G) . n) <> {} ) ;

suppose A5: PRIM:NextBestEdges ((PRIM:CompSeq G) . n) = {} ; :: thesis: S₁[n + 1]

then A6: card (((PRIM:CompSeq G) . n) `1) = card (G .reachableFrom the Element of the_Vertices_of G) by Th35;
then card (G .reachableFrom the Element of the_Vertices_of G) <= n + 1 by A3, XXREAL_0:def 9;
then A7: card (G .reachableFrom the Element of the_Vertices_of G) <= (n + 1) + 1 by NAT_1:12;
card (((PRIM:CompSeq G) . (n + 1)) `1) = min ((n + 1),(card (G .reachableFrom the Element of the_Vertices_of G))) by A3, A4, A5, Def15;
hence S₁[n + 1] by A3, A6, A7, XXREAL_0:def 9; :: thesis: verum

end;

suppose A8: PRIM:NextBestEdges ((PRIM:CompSeq G) . n) <> {} ; :: thesis: S₁[n + 1]

A9: ((PRIM:CompSeq G) . n) `1 c= G .reachableFrom the Element of the_Vertices_of G by Th33;
A10: ((PRIM:CompSeq G) . n) `1 <> G .reachableFrom the Element of the_Vertices_of G by A8, Th35;

A11: now :: thesis: not card (((PRIM:CompSeq G) . n) `1) = card (G .reachableFrom the Element of the_Vertices_of G)

assume A12: card (((PRIM:CompSeq G) . n) `1) = card (G .reachableFrom the Element of the_Vertices_of G) ; :: thesis: contradiction
((PRIM:CompSeq G) . n) `1 c< G .reachableFrom the Element of the_Vertices_of G by A10, A9, XBOOLE_0:def 8;
hence contradiction by A12, CARD_2:48; :: thesis: verum

end;

then A13: card (((PRIM:CompSeq G) . n) `1) = n + 1 by A3, XXREAL_0:15;
consider v being Vertex of G such that
A14: not v in ((PRIM:CompSeq G) . n) `1 and
A15: (PRIM:CompSeq G) . (n + 1) = [((((PRIM:CompSeq G) . n) `1) \/ {v}),((((PRIM:CompSeq G) . n) `2) \/ { the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n)})] by A4, A8, Th28;
A16: card (((PRIM:CompSeq G) . (n + 1)) `1) = card ((((PRIM:CompSeq G) . n) `1) \/ {v}) by A15
.= (card (((PRIM:CompSeq G) . n) `1)) + 1 by A14, CARD_2:41 ;
card (((PRIM:CompSeq G) . n) `1) <= card (G .reachableFrom the Element of the_Vertices_of G) by Th33, NAT_1:43;
then n + 1 < card (G .reachableFrom the Element of the_Vertices_of G) by A11, A13, XXREAL_0:1;
then (n + 1) + 1 <= card (G .reachableFrom the Element of the_Vertices_of G) by NAT_1:13;
hence S₁[n + 1] by A16, A13, XXREAL_0:def 9; :: thesis: verum

end;

end;

end;

hence S₁[n + 1] ; :: thesis: verum

end;

(PRIM:CompSeq G) . 0 = PRIM:Init G by Def17;
then { the Element of the_Vertices_of G} = ((PRIM:CompSeq G) . 0) `1 ;
then card (((PRIM:CompSeq G) . 0) `1) = 1 by CARD_1:30;
then A17: S₁[ 0 ] by A1, XXREAL_0:def 9;
for n being Nat holds S₁[n] from NAT_1:sch 2(A17, A2);
hence for n being Nat holds card (((PRIM:CompSeq G) . n) `1) = min ((n + 1),(card (G .reachableFrom the Element of the_Vertices_of G))) ; :: thesis: verum