( <%(f . 0)%> . 0 = f . 0 & len f = 1 ) by CARD_1:def 7;
hence <%(f . 0)%> = f by AFINSQ_1:34; :: thesis: verum