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