thus
union X is Function-like
union X is Relation-like proof
let x,
y1,
y2 be
object ;
FUNCT_1:def 1 ( 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
;
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;
verum
end;
thus
union X is Relation-like
verum