let a be set ; :: thesis: 1 |-> a = <*a*>
1 in Seg 1 ;
then ( len (1 |-> a) = 1 & (1 |-> a) . 1 = a ) by FINSEQ_1:def 18, FUNCOP_1:13;
hence 1 |-> a = <*a*> by FINSEQ_1:57; :: thesis: verum