let X be non empty finite set ; :: thesis: 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
let R be Equivalence_Relation of X; :: thesis: for S being Class R -valued Function
for i being set st i in dom S holds
S . i is finite Subset of X
let S be Class R -valued Function; :: thesis: for i being set st i in dom S holds
S . i is finite Subset of X
let i be set ; :: thesis: ( i in dom S implies S . i is finite Subset of X )
assume i in dom S ; :: thesis: S . i is finite Subset of X
then S . i in Class R by FUNCT_1:102;
hence S . i is finite Subset of X ; :: thesis: verum