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