theorem :: FUNCT_4:129

for a, b, c, x, y, z being object holds rng ((a,b,c) --> (x,y,z)) c= {x,y,z}