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:
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 ;
consider fx being set such that
A8: [x,y1] in fx and
A9: fx in X by ;
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 b1, b2 being object st x = [b1,b2] )
assume x in union X ; :: thesis: ex b1, b2 being object st x = [b1,b2]
then ex ux being set st
( x in ux & ux in X ) by TARSKI:def 4;
hence ex b1, b2 being object st x = [b1,b2] by RELAT_1:def 1; :: thesis: verum
end;
hence union X is Function by A2; :: thesis: verum