let A, B, Y be set ; :: thesis: ( Y c= Funcs (A,B) implies union Y c= [:A,B:] )
set AB = [:A,B:];
set F = Funcs (A,B);
set X = Y;
assume Y c= Funcs (A,B) ; :: thesis: union Y c= [:A,B:]
then ( Y c= Funcs (A,B) & Funcs (A,B) c= bool [:A,B:] ) by FRAENKEL:2;
then reconsider XX = Y as Subset of (bool [:A,B:]) by XBOOLE_1:1;
union XX is Subset of [:A,B:] ;
hence union Y c= [:A,B:] ; :: thesis: verum