theorem :: FINSEQ_1:99

for x1, x2 being object holds <*x1,x2*> = {[1,x1],[2,x2]}