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 A1: ( [x,y1] in union X & [x,y2] in union X ) ; :: thesis: y1 = y2
then consider f being set such that
A2: ( [x,y1] in f & f in X ) by TARSKI:def 4;
consider g being set such that
A3: ( [x,y2] in g & g in X ) by A1, TARSKI:def 4;
reconsider f = f, g = g as Function by A2, A3;
A4: ( x in dom f & x in dom g ) by A2, A3, RELAT_1:def 4;
then A5: ( f . x = y1 & g . x = y2 ) by A2, A3, FUNCT_1:def 4;
A6: x in (dom f) /\ (dom g) by A4, XBOOLE_0:def 4;
f tolerates g by A2, A3, Def1;
hence y1 = y2 by A5, A6, PARTFUN1:def 6; :: 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 consider f being set such that
A7: ( x in f & f in X ) by TARSKI:def 4;
consider y, z being set such that
A8: x = [y,z] by A7, RELAT_1:def 1;
thus ex b₁, b₂ being set st x = [b₁,b₂] by A8; :: thesis: verum

end;