let S be non empty Graph-membered vertex-disjoint set ; :: thesis: card S = card { (H .componentSet()) where H is Element of S : verum }
deffunc H1( Element of S) -> Element of bool (bool (the_Vertices_of $1)) = $1 .componentSet() ;
consider f being ManySortedSet of S such that
A1: for H being Element of S holds f . H = H1(H) from PBOOLE:sch 5();
 A2: dom f = S by PARTFUN1:def 2;
set M = { (H .componentSet()) where H is Element of S : verum } ;
now :: thesis: for y being object holds
( ( y in rng f implies y in { (H .componentSet()) where H is Element of S : verum } ) & ( y in { (H .componentSet()) where H is Element of S : verum } implies y in rng f ) )
let y be object ; :: thesis: ( ( y in rng f implies y in { (H .componentSet()) where H is Element of S : verum } ) & ( y in { (H .componentSet()) where H is Element of S : verum } implies y in rng f ) )
hereby :: thesis: ( y in { (H .componentSet()) where H is Element of S : verum } implies y in rng f )
assume y in rng f ; :: thesis: y in { (H .componentSet()) where H is Element of S : verum }
then consider x being object such that
A3: ( x in dom f & f . x = y ) by FUNCT_1:def 3;
reconsider x = x as Element of S by A3;
y = x .componentSet() by A1, A3;
hence y in { (H .componentSet()) where H is Element of S : verum } ; :: thesis: verum
end;
assume y in { (H .componentSet()) where H is Element of S : verum } ; :: thesis: y in rng f
then consider H being Element of S such that
A4: y = H .componentSet() ;
f . H in rng f by A2, FUNCT_1:3;
hence y in rng f by A1, A4; :: thesis: verum
end;
then A5: rng f = { (H .componentSet()) where H is Element of S : verum } by TARSKI:2;
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 A6: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
then reconsider H1 = x1, H2 = x2 as Element of S ;
set V = the Element of H1 .componentSet() ;
( f . x1 = H1 .componentSet() & f . x2 = H2 .componentSet() ) by A1;
then ( the Element of H1 .componentSet() in H1 .componentSet() & the Element of H1 .componentSet() in H2 .componentSet() ) by A6;
then A7: the Element of H1 .componentSet() c= (the_Vertices_of H1) /\ (the_Vertices_of H2) by XBOOLE_1:19;
(the_Vertices_of H1) /\ (the_Vertices_of H2) <> {} by A7;
hence x1 = x2 by Def18, XBOOLE_0:def 7; :: thesis: verum
end;
hence card S = card { (H .componentSet()) where H is Element of S : verum } by A2, A5, FUNCT_1:def 4, CARD_1:70; :: thesis: verum