let a be object ; :: thesis: 1 |-> a = <*a*>
1 in Seg 1 ;
then ( len (1 |-> a) = 1 & (1 |-> a) . 1 = a ) by CARD_1:def 7, FUNCOP_1:7;
hence 1 |-> a = <*a*> by FINSEQ_1:40; :: thesis: verum