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 S = X
let R be Equivalence_Relation of X; :: thesis: for S being Class R -valued Function st S is onto holds
Union S = X
let S be Class R -valued Function; :: thesis: ( S is onto implies Union S = X )
assume A1: S is onto ; :: thesis: Union S = X
union (Class R) = X by EQREL_1:def 4;
hence Union S = X by A1, FUNCT_2:def 3; :: thesis: verum