set U = union (rng f);
union (rng f) is Relation-like

proof

let x be object ; :: according to RELAT_1:def 1 :: thesis: ( not x in union (rng f) or ex b₁, b₂ being object st x = [b₁,b₂] )
assume x in union (rng f) ; :: thesis: ex b₁, b₂ being object st x = [b₁,b₂]
then consider Y being set such that
A1: ( x in Y & Y in rng f ) by TARSKI:def 4;
consider X being object such that
A2: ( X in dom f & f . X = Y ) by A1, FUNCT_1:def 3;
thus ex b₁, b₂ being object st x = [b₁,b₂] by A1, A2, RELAT_1:def 1; :: thesis: verum

end;

then reconsider U = union (rng f) as Relation ;
for x, y1, y2 being object st [x,y1] in U & [x,y2] in U holds
y1 = y2

proof

let x, y1, y2 be object ; :: thesis: ( [x,y1] in U & [x,y2] in U implies y1 = y2 )
assume A3: ( [x,y1] in U & [x,y2] in U ) ; :: thesis: y1 = y2
consider Y1 being set such that
A4: ( [x,y1] in Y1 & Y1 in rng f ) by A3, TARSKI:def 4;
consider z1 being object such that
A5: ( z1 in dom f & f . z1 = Y1 ) by FUNCT_1:def 3, A4;
consider Y2 being set such that
A6: ( [x,y2] in Y2 & Y2 in rng f ) by A3, TARSKI:def 4;
consider z2 being object such that
A7: ( z2 in dom f & f . z2 = Y2 ) by FUNCT_1:def 3, A6;
reconsider z1 = z1, z2 = z2 as Ordinal by A5, A7;
( z1 c= z2 or z2 c= z1 ) ;
then ( f . z1 c= f . z2 or f . z2 c= f . z1 ) by A5, A7, COHSP_1:def 11;
hence y1 = y2 by FUNCT_1:def 1, A4, A6, A5, A7; :: thesis: verum

end;

hence ( union (rng f) is Function-like & union (rng f) is Relation-like ) by FUNCT_1:def 1; :: thesis: verum