( <*(f . 1)*> . 1 = f . 1 & len f = 1 ) by CARD_1:def 7;
hence <*(f . 1)*> = f by FINSEQ_1:40; :: thesis: verum