theorem Th54: :: EC_PF_1:54

for X being non empty finite set
for R being Equivalence_Relation of X
for S being Class b₂ -valued Function
for i being set st i in dom S holds
S . i is finite Subset of X