theorem Th142: :: FUNCT_4:142

for a, b, c, x, y, z, w, d being object st x <> y & x <> w & x <> z holds
((x,y,w,z) --> (a,b,c,d)) . x = a