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