let X be functional set ; :: thesis: ( ( for f, g being Function st f in X & g in X holds
f tolerates g ) implies union X is Function )
assume A1: for f, g being Function st f in X & g in X holds
f tolerates g ; :: thesis: union X is Function
A2: union X is Function-like

proof

let x, y1, y2 be object ; :: 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
A3: [x,y1] in union X and
A4: [x,y2] in union X and
A5: y1 <> y2 ; :: thesis: contradiction
consider gx being set such that
A6: [x,y2] in gx and
A7: gx in X by A4, TARSKI:def 4;
consider fx being set such that
A8: [x,y1] in fx and
A9: fx in X by A3, TARSKI:def 4;
reconsider fx = fx, gx = gx as Function by A9, A7;
fx tolerates gx by A1, A9, A7;
then ex h being Function st
( fx c= h & gx c= h ) by PARTFUN1:52;
hence contradiction by A5, A8, A6, FUNCT_1:def 1; :: thesis: verum

end;

union X is Relation-like

proof

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

end;

hence union X is Function by A2; :: thesis: verum