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; ( 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; 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; verum