let a be set ; :: thesis: (*--> a) . 0 = {}
thus (*--> a) . 0 = 0 |-> a by FINSEQ_2:def 6
.= {} ; :: thesis: verum