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