let X be set ; :: thesis: ( ( X is functional & X is compatible ) iff union X is Function )

A1: now

assume A2: union X is Function ; :: thesis: ( X is functional & X is compatible )
thus X is functional :: thesis: X is compatible

proof

let f be set ; :: according to FUNCT_1:def 19 :: thesis: ( not f in X or f is set )
assume A3: f in X ; :: thesis: f is set
A4: f is Function-like

proof

let x, y1, y2 be set ; :: according to FUNCT_1:def 1 :: thesis: ( not [x,y1] in f or not [x,y2] in f or y1 = y2 )
assume ( [x,y1] in f & [x,y2] in f ) ; :: thesis: y1 = y2
then ( [x,y1] in union X & [x,y2] in union X ) by A3, TARSKI:def 4;
hence y1 = y2 by A2, FUNCT_1:def 1; :: thesis: verum

end;

f is Relation-like

proof

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

end;

hence f is set by A4; :: thesis: verum

end;

thus X is compatible :: thesis: verum

proof

let f, g be Function; :: according to COMPUT_1:def 1 :: thesis: ( f in X & g in X implies f tolerates g )
assume A5: ( f in X & g in X ) ; :: thesis: f tolerates g
let x be set ; :: according to PARTFUN1:def 6 :: thesis: ( not x in (dom f) /\ (dom g) or f . x = g . x )
assume x in (dom f) /\ (dom g) ; :: thesis: f . x = g . x
then A6: ( x in dom f & x in dom g ) by XBOOLE_0:def 4;
then consider y1 being set such that
A7: [x,y1] in f by RELAT_1:def 4;
consider y2 being set such that
A8: [x,y2] in g by A6, RELAT_1:def 4;
( [x,y1] in union X & [x,y2] in union X ) by A5, A7, A8, TARSKI:def 4;
then A9: y1 = y2 by A2, FUNCT_1:def 1;
thus f . x = y1 by A6, A7, FUNCT_1:def 4
.= g . x by A6, A8, A9, FUNCT_1:def 4 ; :: thesis: verum

end;

end;

thus ( ( X is functional & X is compatible ) iff union X is Function ) by A1; :: thesis: verum