( <%(f . 0),(f . 1),(f . 2)%> . 0 = f . 0 & <%(f . 0),(f . 1),(f . 2)%> . 1 = f . 1 & <%(f . 0),(f . 1),(f . 2)%> . 2 = f . 2 & len f = 3 ) by CARD_1:def 7;
hence <%(f . 0),(f . 1),(f . 2)%> = f by AFINSQ_1:39; :: thesis: verum