theorem :: ANPROJ10:1

for a, b, c, d, a9, b9, c9, d9 being object st <*a,b,c,d*> = <*a9,b9,c9,d9*> holds
( a = a9 & b = b9 & c = c9 & d = d9 )