<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 ( len (<*<e1>*> @) = 3 & (<*<e1>*> @) . 1 = <*1*> & (<*<e1>*> @) . 2 = <*0*> & (<*<e1>*> @) . 3 = <*0*> )thus
len (<*<e1>*> @) = 3
by MATRIX_0:def 6, A4;
( (<*<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
;
( (<*<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
;
(<*<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
;
verum end;
hence
<*<e1>*> @ = <*<*1*>,<*0*>,<*0*>*>
by FINSEQ_1:45; ( <*<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 ( len (<*<e2>*> @) = 3 & (<*<e2>*> @) . 1 = <*0*> & (<*<e2>*> @) . 2 = <*1*> & (<*<e2>*> @) . 3 = <*0*> )thus
len (<*<e2>*> @) = 3
by MATRIX_0:def 6, A13bis;
( (<*<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
;
( (<*<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
;
(<*<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
;
verum end;
hence
<*<e2>*> @ = <*<*0*>,<*1*>,<*0*>*>
by FINSEQ_1:45; <*<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 ( len (<*<e3>*> @) = 3 & (<*<e3>*> @) . 1 = <*0*> & (<*<e3>*> @) . 2 = <*0*> & (<*<e3>*> @) . 3 = <*1*> )thus A25:
len (<*<e3>*> @) = 3
by MATRIX_0:def 6, A23;
( (<*<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
;
( (<*<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
;
(<*<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
;
verum end;
hence
<*<e3>*> @ = <*<*0*>,<*0*>,<*1*>*>
by FINSEQ_1:45; verum