theorem Th16: :: HILB10_7:16

for x, y being object
for X, Y being set holds Ext ((X \/ Y),x,y) = (Ext (X,x,y)) \/ (Ext (Y,x,y))