let A be set ; ( 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
; FUNCT_1:def 13 union A is Function
A3:
now for x, y, z being object st [x,y] in union A & [x,z] in union A holds
y = zlet x,
y,
z be
object ;
( [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
;
y = zconsider 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;
verum end;
hence
union A is Function
by A3, FUNCT_1:def 1, RELAT_1:def 1; verum