let A be set ; :: thesis: ( A is functional & ( 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 object 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 ; :: according to FUNCT_1:def 13 :: thesis: union A is Function

A3: now :: thesis: for x, y, z being object st [x,y] in union A & [x,z] in union A holds
y = z

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

end;

now :: thesis: for z being object st z in union A holds
ex x, y being object st [x,y] = z

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

end;

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