<e1> in REAL 3 ;
then A1: <e1> in 3 -tuples_on REAL by EUCLID:def 1;
A2: len <*<e1>*> = 1 by FINSEQ_1:39;
rng <*<e1>*> = {<e1>} by FINSEQ_1:39;
then <e1> in rng <*<e1>*> by TARSKI:def 1;
then A4: width <*<e1>*> = len <e1> by A2, MATRIX_0:def 3
.= 3 by A1, FINSEQ_2:133 ;
A5: width (<*<e1>*> @) = len <*<e1>*> by A4, MATRIX_0:29
.= 1 by FINSEQ_1:39 ;

now :: thesis: ( len (<*<e1>*> @) = 3 & (<*<e1>*> @) . 1 = <*1*> & (<*<e1>*> @) . 2 = <*0*> & (<*<e1>*> @) . 3 = <*0*> )

thus len (<*<e1>*> @) = 3 by MATRIX_0:def 6, A4; :: thesis: ( (<*<e1>*> @) . 1 = <*1*> & (<*<e1>*> @) . 2 = <*0*> & (<*<e1>*> @) . 3 = <*0*> )
then A7: <*<e1>*> @ is Matrix of 3,1,F_Real by A5, MATRIX_0:20;
A8: 1 in Seg 3 by FINSEQ_1:1;
hence (<*<e1>*> @) . 1 = Line ((<*<e1>*> @),1) by A7, MATRIX_0:52
.= <*1*> by A8, A4, MATRIX_0:59, Th52 ;
:: thesis: ( (<*<e1>*> @) . 2 = <*0*> & (<*<e1>*> @) . 3 = <*0*> )
A9: 2 in Seg 3 by FINSEQ_1:1;
hence (<*<e1>*> @) . 2 = Line ((<*<e1>*> @),2) by A7, MATRIX_0:52
.= <*0*> by A9, A4, MATRIX_0:59, Th52 ;
:: thesis: (<*<e1>*> @) . 3 = <*0*>
A10: 3 in Seg 3 by FINSEQ_1:1;
hence (<*<e1>*> @) . 3 = Line ((<*<e1>*> @),3) by A7, MATRIX_0:52
.= <*0*> by A10, A4, MATRIX_0:59, Th52 ;
:: thesis: verum

end;

hence <*<e1>*> @ = <*<*1*>,<*0*>,<*0*>*> by FINSEQ_1:45; :: thesis: ( <*<e2>*> @ = <*<*0*>,<*1*>,<*0*>*> & <*<e3>*> @ = <*<*0*>,<*0*>,<*1*>*> )
<e2> in REAL 3 ;
then A11: <e2> in 3 -tuples_on REAL by EUCLID:def 1;
A12: len <*<e2>*> = 1 by FINSEQ_1:39;
rng <*<e2>*> = {<e2>} by FINSEQ_1:39;
then <e2> in rng <*<e2>*> by TARSKI:def 1;
then A13bis: width <*<e2>*> = len <e2> by A12, MATRIX_0:def 3
.= 3 by A11, FINSEQ_2:133 ;
then A14: width (<*<e2>*> @) = len <*<e2>*> by MATRIX_0:29
.= 1 by FINSEQ_1:39 ;

now :: thesis: ( len (<*<e2>*> @) = 3 & (<*<e2>*> @) . 1 = <*0*> & (<*<e2>*> @) . 2 = <*1*> & (<*<e2>*> @) . 3 = <*0*> )

thus len (<*<e2>*> @) = 3 by MATRIX_0:def 6, A13bis; :: thesis: ( (<*<e2>*> @) . 1 = <*0*> & (<*<e2>*> @) . 2 = <*1*> & (<*<e2>*> @) . 3 = <*0*> )
then A16: <*<e2>*> @ is Matrix of 3,1,F_Real by A14, MATRIX_0:20;
A17: 1 in Seg 3 by FINSEQ_1:1;
hence (<*<e2>*> @) . 1 = Line ((<*<e2>*> @),1) by A16, MATRIX_0:52
.= <*0*> by A17, A13bis, MATRIX_0:59, Th53 ;
:: thesis: ( (<*<e2>*> @) . 2 = <*1*> & (<*<e2>*> @) . 3 = <*0*> )
A18: 2 in Seg 3 by FINSEQ_1:1;
hence (<*<e2>*> @) . 2 = Line ((<*<e2>*> @),2) by A16, MATRIX_0:52
.= <*1*> by A18, A13bis, MATRIX_0:59, Th53 ;
:: thesis: (<*<e2>*> @) . 3 = <*0*>
A19: 3 in Seg 3 by FINSEQ_1:1;
hence (<*<e2>*> @) . 3 = Line ((<*<e2>*> @),3) by A16, MATRIX_0:52
.= <*0*> by A19, A13bis, MATRIX_0:59, Th53 ;
:: thesis: verum

end;

hence <*<e2>*> @ = <*<*0*>,<*1*>,<*0*>*> by FINSEQ_1:45; :: thesis: <*<e3>*> @ = <*<*0*>,<*0*>,<*1*>*>
<e3> in REAL 3 ;
then A20: <e3> in 3 -tuples_on REAL by EUCLID:def 1;
A21: len <*<e3>*> = 1 by FINSEQ_1:39;
rng <*<e3>*> = {<e3>} by FINSEQ_1:39;
then <e3> in rng <*<e3>*> by TARSKI:def 1;
then A23: width <*<e3>*> = len <e3> by A21, MATRIX_0:def 3
.= 3 by A20, FINSEQ_2:133 ;
A24: width (<*<e3>*> @) = len <*<e3>*> by A23, MATRIX_0:29
.= 1 by FINSEQ_1:39 ;

now :: thesis: ( len (<*<e3>*> @) = 3 & (<*<e3>*> @) . 1 = <*0*> & (<*<e3>*> @) . 2 = <*0*> & (<*<e3>*> @) . 3 = <*1*> )

thus A25: len (<*<e3>*> @) = 3 by MATRIX_0:def 6, A23; :: thesis: ( (<*<e3>*> @) . 1 = <*0*> & (<*<e3>*> @) . 2 = <*0*> & (<*<e3>*> @) . 3 = <*1*> )
A26: <*<e3>*> @ is Matrix of 3,1,F_Real by A25, A24, MATRIX_0:20;
A27: 1 in Seg 3 by FINSEQ_1:1;
hence (<*<e3>*> @) . 1 = Line ((<*<e3>*> @),1) by A26, MATRIX_0:52
.= <*0*> by A27, A23, MATRIX_0:59, Th54 ;
:: thesis: ( (<*<e3>*> @) . 2 = <*0*> & (<*<e3>*> @) . 3 = <*1*> )
A28: 2 in Seg 3 by FINSEQ_1:1;
hence (<*<e3>*> @) . 2 = Line ((<*<e3>*> @),2) by A26, MATRIX_0:52
.= <*0*> by A28, A23, MATRIX_0:59, Th54 ;
:: thesis: (<*<e3>*> @) . 3 = <*1*>
A29: 3 in Seg 3 by FINSEQ_1:1;
hence (<*<e3>*> @) . 3 = Line ((<*<e3>*> @),3) by A26, MATRIX_0:52
.= <*1*> by A29, A23, MATRIX_0:59, Th54 ;
:: thesis: verum

end;

hence <*<e3>*> @ = <*<*0*>,<*0*>,<*1*>*> by FINSEQ_1:45; :: thesis: verum