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) . b₁ misses (S | X) . b₂ )
assume A2: x <> y ; :: thesis: (S | X) . b₁ misses (S | X) . b₂

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) . b₁ misses (S | X) . b₂

then ( (S | X) . x = S . x & (S | X) . y = S . y ) by FUNCT_1:47;
hence (S | X) . x misses (S | X) . y by A1, A2, PROB_2:def 2; :: thesis: verum

end;

suppose A3: ( not x in dom (S | X) or not y in dom (S | X) ) ; :: thesis: (S | X) . b₁ misses (S | X) . b₂

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