A1: len (1. (F_Real,3)) = 3 by MATRIX_0:23;
( 1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 ) by FINSEQ_1:1;
then ( (1. (F_Real,3)) . 1 = Line ((1. (F_Real,3)),1) & (1. (F_Real,3)) . 2 = Line ((1. (F_Real,3)),2) & (1. (F_Real,3)) . 3 = Line ((1. (F_Real,3)),3) ) by MATRIX_0:52;
hence 1. (F_Real,3) = <*<*1,0,0*>,<*0,1,0*>,<*0,0,1*>*> by A1, FINSEQ_1:45, ANPROJ_8:68; :: thesis: verum