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