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 Relation-like

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 ux being set such that
A3: ( x in ux & ux in X ) by TARSKI:def 4;
thus ex b₁, b₂ being set st x = [b₁,b₂] by A3, RELAT_1:def 1; :: thesis: verum

end;

union X is Function-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 A4: ( [x,y1] in union X & [x,y2] in union X & y1 <> y2 ) ; :: thesis: contradiction
then consider fx being set such that
A5: ( [x,y1] in fx & fx in X ) by TARSKI:def 4;
consider gx being set such that
A6: ( [x,y2] in gx & gx in X ) by A4, TARSKI:def 4;
reconsider fx = fx, gx = gx as Function by A5, A6;
fx tolerates gx by A1, A5, A6;
then consider h being Function such that
A7: ( fx c= h & gx c= h ) by PARTFUN1:131;
thus contradiction by A4, A5, A6, A7, FUNCT_1:def 1; :: thesis: verum

end;

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