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

proof

let x, y1, y2 be set ; :: 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: x in dom f by A3, RELAT_1:def 4;
then A8: f . x = y1 by A3, FUNCT_1:def 2;
A9: x in dom g by A5, RELAT_1:def 4;
then A10: g . x = y2 by A5, FUNCT_1:def 2;
A11: x in (dom f) /\ (dom g) by A7, A9, XBOOLE_0:def 4;
f tolerates g by A4, A6, Def1;
hence y1 = y2 by A8, A10, A11, PARTFUN1:def 4; :: thesis: verum

end;

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

proof

let x be set ; :: according to RELAT_1:def 1 :: thesis: ( not x in union X or ex b₁, b₂ being set st x = [b₁,b₂] )
assume x in union X ; :: thesis: ex b₁, b₂ being set 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 set st x = [b₁,b₂] by RELAT_1:def 1; :: thesis: verum

end;