let X be non empty set ; :: thesis: for R being Equivalence_Relation of X
for S being Class b₁ -valued Function st S is onto holds
union (rng S) = X
let R be Equivalence_Relation of X; :: thesis: for S being Class R -valued Function st S is onto holds
union (rng S) = X
let S be Class R -valued Function; :: thesis: ( S is onto implies union (rng S) = X )
assume AS: S is onto ; :: thesis: union (rng S) = X
union (Class R) = X by EQREL_1:def 6;
hence union (rng S) = X by AS, FUNCT_2:def 3; :: thesis: verum