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