let S be Function; :: thesis: for X being set st S is disjoint_valued holds
S | X is disjoint_valued

let X be set ; :: thesis: ( S is disjoint_valued implies S | X is disjoint_valued )
assume A1: S is disjoint_valued ; :: thesis: S | X is disjoint_valued
set SN = S | X;
now :: thesis: for x, y being object st x <> y holds
(S | X) . x misses (S | X) . y
let x, y be object ; :: thesis: ( x <> y implies (S | X) . b1 misses (S | X) . b2 )
assume A2: x <> y ; :: thesis: (S | X) . b1 misses (S | X) . b2
per cases ( ( x in dom (S | X) & y in dom (S | X) ) or not x in dom (S | X) or not y in dom (S | X) ) ;
suppose ( x in dom (S | X) & y in dom (S | X) ) ; :: thesis: (S | X) . b1 misses (S | X) . b2
then ( (S | X) . x = S . x & (S | X) . y = S . y ) by FUNCT_1:47;
hence (S | X) . x misses (S | X) . y by ; :: thesis: verum
end;
suppose A3: ( not x in dom (S | X) or not y in dom (S | X) ) ; :: thesis: (S | X) . b1 misses (S | X) . b2
now :: thesis: (S | X) . x misses (S | X) . y
per cases ( not x in dom (S | X) or not y in dom (S | X) ) by A3;
suppose not x in dom (S | X) ; :: thesis: (S | X) . x misses (S | X) . y
then (S | X) . x = {} by FUNCT_1:def 2;
then ((S | X) . x) /\ ((S | X) . y) = {} ;
hence (S | X) . x misses (S | X) . y ; :: thesis: verum
end;
suppose not y in dom (S | X) ; :: thesis: (S | X) . x misses (S | X) . y
then (S | X) . y = {} by FUNCT_1:def 2;
then ((S | X) . x) /\ ((S | X) . y) = {} ;
hence (S | X) . x misses (S | X) . y ; :: thesis: verum
end;
end;
end;
hence (S | X) . x misses (S | X) . y ; :: thesis: verum
end;
end;
end;
hence S | X is disjoint_valued by PROB_2:def 2; :: thesis: verum