theorem :: FOMODEL0:19

for A, B, Y being set st Y c= Funcs (A,B) holds
union Y c= [:A,B:] by Lm2;