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