theorem :: FINSEQ_1:77

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