let UN be Universe; :: thesis: for I, a, b, u, v being Element of UN
for x being UN -valued ManySortedSet of I st I = {a,b} & x . a = u & x . b = v holds
disjoint-union x = [:u,{a}:] \/ [:v,{b}:]
let I, a, b, u, v be Element of UN; :: thesis: for x being UN -valued ManySortedSet of I st I = {a,b} & x . a = u & x . b = v holds
disjoint-union x = [:u,{a}:] \/ [:v,{b}:]
let x be UN -valued ManySortedSet of I; :: thesis: ( I = {a,b} & x . a = u & x . b = v implies disjoint-union x = [:u,{a}:] \/ [:v,{b}:] )
assume that
A1: I = {a,b} and
A2: x . a = u and
A3: x . b = v ; :: thesis: disjoint-union x = [:u,{a}:] \/ [:v,{b}:]
A4: ( dom (disjoin x) = dom x & ( for o being object st o in dom x holds
(disjoin x) . o = [:(x . o),{o}:] ) ) by CARD_3:def 3;
A5: dom x = {a,b} by A1, PARTFUN1:def 2;
then ( a in dom x & b in dom x ) by TARSKI:def 2;
then A6: ( (disjoin x) . a = [:(x . a),{a}:] & (disjoin x) . b = [:(x . b),{b}:] ) by CARD_3:def 3;
set S = {[:(x . a),{a}:],[:(x . b),{b}:]};
rng (disjoin x) = {[:(x . a),{a}:],[:(x . b),{b}:]}

proof

now :: thesis: ( rng (disjoin x) c= {[:(x . a),{a}:],[:(x . b),{b}:]} & {[:(x . a),{a}:],[:(x . b),{b}:]} c= rng (disjoin x) )

now :: thesis: for o being object st o in rng (disjoin x) holds
o in {[:(x . a),{a}:],[:(x . b),{b}:]}

let o be object ; :: thesis: ( o in rng (disjoin x) implies o in {[:(x . a),{a}:],[:(x . b),{b}:]} )
assume o in rng (disjoin x) ; :: thesis: o in {[:(x . a),{a}:],[:(x . b),{b}:]}
then consider o9 being object such that
A7: o9 in dom (disjoin x) and
A8: o = (disjoin x) . o9 by FUNCT_1:def 3;
( o9 = a or o9 = b ) by A7, A4, A5, TARSKI:def 2;
hence o in {[:(x . a),{a}:],[:(x . b),{b}:]} by A8, A6, TARSKI:def 2; :: thesis: verum

end;

hence rng (disjoin x) c= {[:(x . a),{a}:],[:(x . b),{b}:]} ; :: thesis: {[:(x . a),{a}:],[:(x . b),{b}:]} c= rng (disjoin x)

now :: thesis: for o being object st o in {[:(x . a),{a}:],[:(x . b),{b}:]} holds
o in rng (disjoin x)

let o be object ; :: thesis: ( o in {[:(x . a),{a}:],[:(x . b),{b}:]} implies o in rng (disjoin x) )
assume o in {[:(x . a),{a}:],[:(x . b),{b}:]} ; :: thesis: o in rng (disjoin x)
then A9: ( o = (disjoin x) . a or o = (disjoin x) . b ) by A6, TARSKI:def 2;
( a in dom (disjoin x) & b in dom (disjoin x) ) by A4, A5, TARSKI:def 2;
hence o in rng (disjoin x) by A9, FUNCT_1:def 3; :: thesis: verum

end;

hence {[:(x . a),{a}:],[:(x . b),{b}:]} c= rng (disjoin x) ; :: thesis: verum

end;

hence rng (disjoin x) = {[:(x . a),{a}:],[:(x . b),{b}:]} ; :: thesis: verum

end;

hence disjoint-union x = [:u,{a}:] \/ [:v,{b}:] by A2, A3, ZFMISC_1:75; :: thesis: verum