let X, Y be set ; :: thesis: for f being Function holds
( dom <:f,X,Y:> c= dom f & rng <:f,X,Y:> c= rng f )
let f be Function; :: thesis: ( dom <:f,X,Y:> c= dom f & rng <:f,X,Y:> c= rng f )
<:f,X,Y:> c= f by Th22;
hence ( dom <:f,X,Y:> c= dom f & rng <:f,X,Y:> c= rng f ) by RELAT_1:11; :: thesis: verum