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