A1: 0. (F_Real,3,3) = 3 |-> (3 |-> (0. F_Real)) by MATRIX_3:def 1;
3 |-> (0. F_Real) = <*0,0,0*> by FINSEQ_2:62;
hence <*<*0,0,0*>,<*0,0,0*>,<*0,0,0*>*> = 0. (F_Real,3,3) by A1, FINSEQ_2:62; :: thesis: verum