theorem :: FINSEQ_1:37

for x being object holds <*x*> = {[1,x]} ;