( len f = 5 & len <*(f . 1),(f . 2),(f . 3),(f . 4),(f . 5)*> = 5 ) by CARD_1:def 7;
hence <*(f . 1),(f . 2),(f . 3),(f . 4),(f . 5)*> = f by FINSEQ_4:78; :: thesis: verum