let A be set ; :: thesis: ( ( for x being set st x in A holds
x is Function ) & ( for f, g being Function st f in A & g in A holds
f tolerates g ) implies union A is Function )
assume that
A1: for x being set st x in A holds
x is Function and
A2: for f, g being Function st f in A & g in A holds
f tolerates g ; :: thesis: union A is Function

A3: now

let z be set ; :: thesis: ( z in union A implies ex x, y being set st [x,y] = z )
assume z in union A ; :: thesis: ex x, y being set st [x,y] = z
then consider p being set such that
A4: ( z in p & p in A ) by TARSKI:def 4;
reconsider p = p as Function by A1, A4;
p = p ;
hence ex x, y being set st [x,y] = z by A4, RELAT_1:def 1; :: thesis: verum

end;

now

let x, y, z be set ; :: thesis: ( [x,y] in union A & [x,z] in union A implies y = z )
assume A5: ( [x,y] in union A & [x,z] in union A ) ; :: thesis: y = z
then consider p being set such that
A6: ( [x,y] in p & p in A ) by TARSKI:def 4;
consider q being set such that
A7: ( [x,z] in q & q in A ) by A5, TARSKI:def 4;
reconsider p = p, q = q as Function by A1, A6, A7;
p tolerates q by A2, A6, A7;
hence y = z by A6, A7, Th187; :: thesis: verum

end;

hence union A is Function by A3, FUNCT_1:def 1, RELAT_1:def 1; :: thesis: verum