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;

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

hence
S | X is disjoint_valued
by PROB_2:def 2; :: thesis: verum(S | X) . x misses (S | X) . y

let x, y be object ; :: thesis: ( x <> y implies (S | X) . b_{1} misses (S | X) . b_{2} )

assume A2: x <> y ; :: thesis: (S | X) . b_{1} misses (S | X) . b_{2}

end;assume A2: x <> y ; :: thesis: (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) )
;

end;

suppose
( x in dom (S | X) & y in dom (S | X) )
; :: thesis: (S | X) . b_{1} misses (S | X) . b_{2}

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;hence (S | X) . x misses (S | X) . y by A1, A2, PROB_2:def 2; :: thesis: verum

suppose A3:
( not x in dom (S | X) or not y in dom (S | X) )
; :: thesis: (S | X) . b_{1} misses (S | X) . b_{2}

end;

now :: thesis: (S | X) . x misses (S | X) . y

hence
(S | X) . x misses (S | X) . y
; :: thesis: verumend;