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