theorem Th23: :: PARTFUN1:23

for X, Y being set
for f being Function holds
( dom <:f,X,Y:> c= dom f & rng <:f,X,Y:> c= rng f )