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