let UN be Universe; :: thesis: for u, v being Element of UN holds Funcs (u,v) c= { f where f is Function of u,v : verum }
let u, v be Element of UN; :: thesis: Funcs (u,v) c= { f where f is Function of u,v : verum }
set F = { f where f is Function of u,v : verum } ;

now :: thesis: for o being object st o in Funcs (u,v) holds
o in { f where f is Function of u,v : verum }

let o be object ; :: thesis: ( o in Funcs (u,v) implies o in { f where f is Function of u,v : verum } )
assume o in Funcs (u,v) ; :: thesis: o in { f where f is Function of u,v : verum }
then consider f being Function such that
A1: o = f and
A2: dom f = u and
A3: rng f c= v by FUNCT_2:def 2;
reconsider f = f as Function of u,v by A2, A3, FUNCT_2:2;
f in { f where f is Function of u,v : verum } ;
hence o in { f where f is Function of u,v : verum } by A1; :: thesis: verum

end;

hence Funcs (u,v) c= { f where f is Function of u,v : verum } ; :: thesis: verum