thus union X is Function-like :: thesis: union X is Relation-like

proof

let x, y1, y2 be object ; :: according to FUNCT_1:def 1 :: thesis: ( not [x,y1] in union X or not [x,y2] in union X or y1 = y2 )
assume that
A1: [x,y1] in union X and
A2: [x,y2] in union X ; :: thesis: y1 = y2
consider f being set such that
A3: [x,y1] in f and
A4: f in X by A1, TARSKI:def 4;
consider g being set such that
A5: [x,y2] in g and
A6: g in X by A2, TARSKI:def 4;
reconsider f = f, g = g as Function by A4, A6;
A7: ( y1 is set & y2 is set ) by TARSKI:1;
A8: x in dom f by A3, XTUPLE_0:def 12;
then A9: f . x = y1 by A3, FUNCT_1:def 2, A7;
A10: x in dom g by A5, XTUPLE_0:def 12;
then A11: g . x = y2 by A5, FUNCT_1:def 2, A7;
A12: x in (dom f) /\ (dom g) by A8, A10, XBOOLE_0:def 4;
f tolerates g by A4, A6, Def1;
hence y1 = y2 by A9, A11, A12; :: thesis: verum

end;

thus union X is Relation-like :: thesis: verum

proof

let x be object ; :: according to RELAT_1:def 1 :: thesis: ( not x in union X or ex b₁, b₂ being object st x = [b₁,b₂] )
assume x in union X ; :: thesis: ex b₁, b₂ being object st x = [b₁,b₂]
then ex f being set st
( x in f & f in X ) by TARSKI:def 4;
hence ex b₁, b₂ being object st x = [b₁,b₂] by RELAT_1:def 1; :: thesis: verum

end;