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