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