now :: thesis: ( len (Line ((1. (F_Real,3)),1)) = 3 & (Line ((1. (F_Real,3)),1)) . 1 = 1 & (Line ((1. (F_Real,3)),1)) . 2 = 0 & (Line ((1. (F_Real,3)),1)) . 3 = 0 )
thus len (Line ((1. (F_Real,3)),1)) = width (1. (F_Real,3)) by MATRIX_0:def 7
.= 3 by MATRIX_0:23 ; :: thesis: ( (Line ((1. (F_Real,3)),1)) . 1 = 1 & (Line ((1. (F_Real,3)),1)) . 2 = 0 & (Line ((1. (F_Real,3)),1)) . 3 = 0 )
[1,1] in Indices (1. (F_Real,3)) by MATRIX_0:23, Th1;
then (Line ((1. (F_Real,3)),1)) . 1 = 1. F_Real by MATRIX_3:7
.= 1 by STRUCT_0:def 7 ;
hence (Line ((1. (F_Real,3)),1)) . 1 = 1 ; :: thesis: ( (Line ((1. (F_Real,3)),1)) . 2 = 0 & (Line ((1. (F_Real,3)),1)) . 3 = 0 )
[1,2] in Indices (1. (F_Real,3)) by MATRIX_0:23, Th1;
then (Line ((1. (F_Real,3)),1)) . 2 = 0. F_Real by MATRIX_3:8
.= 0 by STRUCT_0:def 6 ;
hence (Line ((1. (F_Real,3)),1)) . 2 = 0 ; :: thesis: (Line ((1. (F_Real,3)),1)) . 3 = 0
[1,3] in Indices (1. (F_Real,3)) by MATRIX_0:23, Th1;
then (Line ((1. (F_Real,3)),1)) . 3 = 0. F_Real by MATRIX_3:8
.= 0 by STRUCT_0:def 6 ;
hence (Line ((1. (F_Real,3)),1)) . 3 = 0 ; :: thesis: verum
end;
hence Line ((1. (F_Real,3)),1) = <*1,0,0*> by FINSEQ_1:45; :: thesis: ( Line ((1. (F_Real,3)),2) = <*0,1,0*> & Line ((1. (F_Real,3)),3) = <*0,0,1*> )
now :: thesis: ( len (Line ((1. (F_Real,3)),2)) = 3 & (Line ((1. (F_Real,3)),2)) . 1 = 0 & (Line ((1. (F_Real,3)),2)) . 2 = 1 & (Line ((1. (F_Real,3)),2)) . 3 = 0 )
thus len (Line ((1. (F_Real,3)),2)) = width (1. (F_Real,3)) by MATRIX_0:def 7
.= 3 by MATRIX_0:23 ; :: thesis: ( (Line ((1. (F_Real,3)),2)) . 1 = 0 & (Line ((1. (F_Real,3)),2)) . 2 = 1 & (Line ((1. (F_Real,3)),2)) . 3 = 0 )
[2,1] in Indices (1. (F_Real,3)) by MATRIX_0:23, Th1;
then (Line ((1. (F_Real,3)),2)) . 1 = 0. F_Real by MATRIX_3:8
.= 0 by STRUCT_0:def 6 ;
hence (Line ((1. (F_Real,3)),2)) . 1 = 0 ; :: thesis: ( (Line ((1. (F_Real,3)),2)) . 2 = 1 & (Line ((1. (F_Real,3)),2)) . 3 = 0 )
[2,2] in Indices (1. (F_Real,3)) by MATRIX_0:23, Th1;
then (Line ((1. (F_Real,3)),2)) . 2 = 1. F_Real by MATRIX_3:7
.= 1 by STRUCT_0:def 7 ;
hence (Line ((1. (F_Real,3)),2)) . 2 = 1 ; :: thesis: (Line ((1. (F_Real,3)),2)) . 3 = 0
[2,3] in Indices (1. (F_Real,3)) by MATRIX_0:23, Th1;
then (Line ((1. (F_Real,3)),2)) . 3 = 0. F_Real by MATRIX_3:8
.= 0 by STRUCT_0:def 6 ;
hence (Line ((1. (F_Real,3)),2)) . 3 = 0 ; :: thesis: verum
end;
hence Line ((1. (F_Real,3)),2) = <*0,1,0*> by FINSEQ_1:45; :: thesis: Line ((1. (F_Real,3)),3) = <*0,0,1*>
now :: thesis: ( len (Line ((1. (F_Real,3)),3)) = 3 & (Line ((1. (F_Real,3)),3)) . 1 = 0 & (Line ((1. (F_Real,3)),3)) . 2 = 0 & (Line ((1. (F_Real,3)),3)) . 3 = 1 )
thus len (Line ((1. (F_Real,3)),3)) = width (1. (F_Real,3)) by MATRIX_0:def 7
.= 3 by MATRIX_0:23 ; :: thesis: ( (Line ((1. (F_Real,3)),3)) . 1 = 0 & (Line ((1. (F_Real,3)),3)) . 2 = 0 & (Line ((1. (F_Real,3)),3)) . 3 = 1 )
[3,1] in Indices (1. (F_Real,3)) by MATRIX_0:23, Th1;
then (Line ((1. (F_Real,3)),3)) . 1 = 0. F_Real by MATRIX_3:8
.= 0 by STRUCT_0:def 6 ;
hence (Line ((1. (F_Real,3)),3)) . 1 = 0 ; :: thesis: ( (Line ((1. (F_Real,3)),3)) . 2 = 0 & (Line ((1. (F_Real,3)),3)) . 3 = 1 )
[3,2] in Indices (1. (F_Real,3)) by MATRIX_0:23, Th1;
then (Line ((1. (F_Real,3)),3)) . 2 = 0. F_Real by MATRIX_3:8
.= 0 by STRUCT_0:def 6 ;
hence (Line ((1. (F_Real,3)),3)) . 2 = 0 ; :: thesis: (Line ((1. (F_Real,3)),3)) . 3 = 1
[3,3] in Indices (1. (F_Real,3)) by MATRIX_0:23, Th1;
then (Line ((1. (F_Real,3)),3)) . 3 = 1. F_Real by MATRIX_3:7
.= 1 by STRUCT_0:def 7 ;
hence (Line ((1. (F_Real,3)),3)) . 3 = 1 ; :: thesis: verum
end;
hence Line ((1. (F_Real,3)),3) = <*0,0,1*> by FINSEQ_1:45; :: thesis: verum