theorem :: FINSEQ_2:62

for a being object holds 3 |-> a = <*a,a,a*>