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

( 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