theorem :: FUNCT_4:146

for a, b, c, d, x, y, z, w, x9, y9, z9, w9 being object st a,b,c,d are_mutually_distinct & (a,b,c,d) --> (x,y,z,w) = (a,b,c,d) --> (x9,y9,z9,w9) holds
( x = x9 & y = y9 & z = z9 & w = w9 )