let X be non empty set ; :: thesis: for R being Equivalence_Relation of X
for S being Class b1 -valued Function st S is one-to-one holds
S is disjoint_valued
let R be Equivalence_Relation of X; :: thesis: for S being Class R -valued Function st S is one-to-one holds
S is disjoint_valued
let S be Class R -valued Function; :: thesis: ( S is one-to-one implies S is disjoint_valued )
assume A1: S is one-to-one ; :: thesis: S is disjoint_valued
now :: thesis: for x, y being object st x <> y holds
S . x misses S . y
let x, y be object ; :: thesis: ( x <> y implies S . b1 misses S . b2 )
assume A2: x <> y ; :: thesis: S . b1 misses S . b2
per cases ( ( x in dom S & y in dom S ) or not x in dom S or not y in dom S ) ;
suppose A3: ( x in dom S & y in dom S ) ; :: thesis: S . b1 misses S . b2
then A4: S . x <> S . y by A1, A2, FUNCT_1:def 4;
( S . x in Class R & S . y in Class R ) by A3, FUNCT_1:102;
hence S . x misses S . y by A4, EQREL_1:def 4; :: thesis: verum
end;
suppose ( not x in dom S or not y in dom S ) ; :: thesis: S . b1 misses S . b2
then ( S . x = {} or S . y = {} ) by FUNCT_1:def 2;
hence S . x misses S . y by XBOOLE_1:65; :: thesis: verum
end;
end;
end;
hence S is disjoint_valued by PROB_2:def 2; :: thesis: verum