let a be set ; :: thesis: (*--> a) . 1 = <*a*>
thus (*--> a) . 1 = 1 |-> a by FINSEQ_2:def 6
.= <*a*> by FINSEQ_2:59 ; :: thesis: verum