let G be _Graph; :: thesis: G .numComponents() = card (G .allComponents())
defpred S₁[ object , object ] means ex H being plain Component of G st
( $1 = H & $2 = the_Vertices_of H );
A1: for x, y1, y2 being object st x in G .allComponents() & S₁[x,y1] & S₁[x,y2] holds
y1 = y2 ;
A2: for x being object st x in G .allComponents() holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis: ( x in G .allComponents() implies ex y being object st S₁[x,y] )
assume x in G .allComponents() ; :: thesis: ex y being object st S₁[x,y]
then reconsider H = x as plain Component of G by Th189;
take the_Vertices_of H ; :: thesis: S₁[x, the_Vertices_of H]
take H ; :: thesis: ( x = H & the_Vertices_of H = the_Vertices_of H )
thus ( x = H & the_Vertices_of H = the_Vertices_of H ) ; :: thesis: verum

end;

consider f being Function such that
A3: dom f = G .allComponents() and
A4: for x being object st x in G .allComponents() holds
S₁[x,f . x] from FUNCT_1:sch 2(A1, A2);

now :: thesis: for y being object holds
( ( y in G .componentSet() implies ex x being object st
( x in dom f & y = f . x ) ) & ( ex x being object st
( x in dom f & y = f . x ) implies y in G .componentSet() ) )

let y be object ; :: thesis: ( ( y in G .componentSet() implies ex x being object st
( x in dom f & y = f . x ) ) & ( ex x being object st
( x in dom f & y = f . x ) implies y in G .componentSet() ) )
thus ( y in G .componentSet() implies ex x being object st
( x in dom f & y = f . x ) ) :: thesis: ( ex x being object st
( x in dom f & y = f . x ) implies y in G .componentSet() )

proof

assume y in G .componentSet() ; :: thesis: ex x being object st
( x in dom f & y = f . x )
then consider v being Vertex of G such that
A5: y = G .reachableFrom v by GLIB_002:def 8;
set H = the plain inducedSubgraph of G,(G .reachableFrom v);
take the plain inducedSubgraph of G,(G .reachableFrom v) ; :: thesis: ( the plain inducedSubgraph of G,(G .reachableFrom v) in dom f & y = f . the plain inducedSubgraph of G,(G .reachableFrom v) )
thus the plain inducedSubgraph of G,(G .reachableFrom v) in dom f by A3, Th189; :: thesis: y = f . the plain inducedSubgraph of G,(G .reachableFrom v)
then consider H9 being plain Component of G such that
A6: ( the plain inducedSubgraph of G,(G .reachableFrom v) = H9 & f . the plain inducedSubgraph of G,(G .reachableFrom v) = the_Vertices_of H9 ) by A3, A4;
thus y = f . the plain inducedSubgraph of G,(G .reachableFrom v) by A5, A6, GLIB_000:def 37; :: thesis: verum

end;

given x being object such that A7: ( x in dom f & y = f . x ) ; :: thesis: y in G .componentSet()
consider H being plain Component of G such that
A8: ( x = H & y = the_Vertices_of H ) by A3, A4, A7;
set v = the Vertex of H;
the_Vertices_of H c= the_Vertices_of G ;
then reconsider v = the Vertex of H as Vertex of G by TARSKI:def 3;
the_Vertices_of H = G .reachableFrom v by GLIB_002:33;
hence y in G .componentSet() by A8, GLIB_002:def 8; :: thesis: verum

end;

then A9: rng f = G .componentSet() by FUNCT_1:def 3;

now :: thesis: for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume A10: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
then consider H1 being plain Component of G such that
A11: ( x1 = H1 & f . x1 = the_Vertices_of H1 ) by A3, A4;
consider H2 being plain Component of G such that
A12: ( x2 = H2 & f . x2 = the_Vertices_of H2 ) by A3, A4, A10;
thus x1 = x2 by A10, A11, A12, GLIB_002:32, GLIB_009:44; :: thesis: verum

end;

then card (G .allComponents()) = card (G .componentSet()) by A3, A9, FUNCT_1:def 4, CARD_1:70;
hence G .numComponents() = card (G .allComponents()) by GLIB_002:def 9; :: thesis: verum