A1: 1. (F_Real,3) = MXF2MXR (1. (F_Real,3)) by MATRIXR1:def 2
.= 1_Rmatrix 3 by MATRIXR2:def 2 ;
A2: [1,1] in Indices (1. (F_Real,3)) by Th1, MATRIX_0:24;
A3: ( 1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 ) by FINSEQ_1:1;
then 1 in dom (1_Rmatrix 3) by Th13;
then A4: (Col ((1_Rmatrix 3),1)) . 1 = (1. (F_Real,3)) * (1,1) by A1, MATRIX_0:def 8
.= 1. F_Real by A2, MATRIX_1:def 3
.= 1 by STRUCT_0:def 7 ;
A5: [2,1] in Indices (1. (F_Real,3)) by Th1, MATRIX_0:24;
2 in dom (1_Rmatrix 3) by A3, Th13;
then A6: (Col ((1_Rmatrix 3),1)) . 2 = (1. (F_Real,3)) * (2,1) by A1, MATRIX_0:def 8
.= 0. F_Real by A5, MATRIX_1:def 3
.= 0 by STRUCT_0:def 6 ;
A7: [3,1] in Indices (1. (F_Real,3)) by Th1, MATRIX_0:24;
3 in dom (1_Rmatrix 3) by A3, Th13;
then A8: (Col ((1_Rmatrix 3),1)) . 3 = (1. (F_Real,3)) * (3,1) by A1, MATRIX_0:def 8
.= 0. F_Real by A7, MATRIX_1:def 3
.= 0 by STRUCT_0:def 6 ;
len (Col ((1_Rmatrix 3),1)) = len (1. (F_Real,3)) by A1, MATRIX_0:def 8
.= 3 by MATRIX_0:24 ;
hence Col ((1. (F_Real,3)),1) = <*1,0,0*> by A1, A4, A6, A8, FINSEQ_1:45; :: thesis: ( Col ((1. (F_Real,3)),2) = <*0,1,0*> & Col ((1. (F_Real,3)),3) = <*0,0,1*> )
A9: [1,2] in Indices (1. (F_Real,3)) by Th1, MATRIX_0:24;
A10: ( 1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 ) by FINSEQ_1:1;
then 1 in dom (1_Rmatrix 3) by Th13;
then A11: (Col ((1_Rmatrix 3),2)) . 1 = (1. (F_Real,3)) * (1,2) by A1, MATRIX_0:def 8
.= 0. F_Real by A9, MATRIX_1:def 3
.= 0 by STRUCT_0:def 6 ;
A12: [2,2] in Indices (1. (F_Real,3)) by Th1, MATRIX_0:24;
2 in dom (1_Rmatrix 3) by A10, Th13;
then A13: (Col ((1_Rmatrix 3),2)) . 2 = (1. (F_Real,3)) * (2,2) by A1, MATRIX_0:def 8
.= 1. F_Real by A12, MATRIX_1:def 3
.= 1 by STRUCT_0:def 7 ;
A14: [3,2] in Indices (1. (F_Real,3)) by Th1, MATRIX_0:24;
3 in dom (1_Rmatrix 3) by A10, Th13;
then A15: (Col ((1_Rmatrix 3),2)) . 3 = (1. (F_Real,3)) * (3,2) by A1, MATRIX_0:def 8
.= 0. F_Real by A14, MATRIX_1:def 3
.= 0 by STRUCT_0:def 6 ;
len (Col ((1_Rmatrix 3),2)) = len (1. (F_Real,3)) by A1, MATRIX_0:def 8
.= 3 by MATRIX_0:24 ;
hence Col ((1. (F_Real,3)),2) = <*0,1,0*> by A1, A11, A13, A15, FINSEQ_1:45; :: thesis: Col ((1. (F_Real,3)),3) = <*0,0,1*>
A16: [1,3] in Indices (1. (F_Real,3)) by Th1, MATRIX_0:24;
A17: ( 1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 ) by FINSEQ_1:1;
then 1 in dom (1_Rmatrix 3) by Th13;
then A18: (Col ((1_Rmatrix 3),3)) . 1 = (1. (F_Real,3)) * (1,3) by A1, MATRIX_0:def 8
.= 0. F_Real by A16, MATRIX_1:def 3
.= 0 by STRUCT_0:def 6 ;
A19: [2,3] in Indices (1. (F_Real,3)) by Th1, MATRIX_0:24;
2 in dom (1_Rmatrix 3) by A17, Th13;
then A20: (Col ((1_Rmatrix 3),3)) . 2 = (1. (F_Real,3)) * (2,3) by A1, MATRIX_0:def 8
.= 0. F_Real by A19, MATRIX_1:def 3
.= 0 by STRUCT_0:def 6 ;
A21: [3,3] in Indices (1. (F_Real,3)) by Th1, MATRIX_0:24;
3 in dom (1_Rmatrix 3) by A17, Th13;
then A22: (Col ((1_Rmatrix 3),3)) . 3 = (1. (F_Real,3)) * (3,3) by A1, MATRIX_0:def 8
.= 1. F_Real by A21, MATRIX_1:def 3
.= 1 by STRUCT_0:def 7 ;
len (Col ((1_Rmatrix 3),3)) = len (1. (F_Real,3)) by A1, MATRIX_0:def 8
.= 3 by MATRIX_0:24 ;
hence Col ((1. (F_Real,3)),3) = <*0,0,1*> by A1, A18, A20, A22, FINSEQ_1:45; :: thesis: verum