let D be non empty set ; for pf being FinSequence of D st len pf = 3 holds
<*pf*> @ = <*<*(pf . 1)*>,<*(pf . 2)*>,<*(pf . 3)*>*>
let pf be FinSequence of D; ( len pf = 3 implies <*pf*> @ = <*<*(pf . 1)*>,<*(pf . 2)*>,<*(pf . 3)*>*> )
assume A1:
len pf = 3
; <*pf*> @ = <*<*(pf . 1)*>,<*(pf . 2)*>,<*(pf . 3)*>*>
A2:
len <*pf*> = 1
by FINSEQ_1:39;
rng <*pf*> = {pf}
by FINSEQ_1:39;
then
pf in rng <*pf*>
by TARSKI:def 1;
then A3:
width <*pf*> = 3
by A1, A2, MATRIX_0:def 3;
then A4: width (<*pf*> @) =
len <*pf*>
by MATRIX_0:29
.=
1
by FINSEQ_1:39
;
now ( len (<*pf*> @) = 3 & (<*pf*> @) . 1 = <*(pf . 1)*> & (<*pf*> @) . 2 = <*(pf . 2)*> & (<*pf*> @) . 3 = <*(pf . 3)*> )thus
len (<*pf*> @) = 3
by MATRIX_0:def 6, A3;
( (<*pf*> @) . 1 = <*(pf . 1)*> & (<*pf*> @) . 2 = <*(pf . 2)*> & (<*pf*> @) . 3 = <*(pf . 3)*> )then A5:
<*pf*> @ is
Matrix of 3,1,
D
by A4, MATRIX_0:20;
1
in Seg 3
by FINSEQ_1:1;
hence (<*pf*> @) . 1 =
Line (
(<*pf*> @),1)
by A5, MATRIX_0:52
.=
<*(pf . 1)*>
by A1, Th62
;
( (<*pf*> @) . 2 = <*(pf . 2)*> & (<*pf*> @) . 3 = <*(pf . 3)*> )
2
in Seg 3
by FINSEQ_1:1;
hence (<*pf*> @) . 2 =
Line (
(<*pf*> @),2)
by A5, MATRIX_0:52
.=
<*(pf . 2)*>
by A1, Th62
;
(<*pf*> @) . 3 = <*(pf . 3)*>
3
in Seg 3
by FINSEQ_1:1;
hence (<*pf*> @) . 3 =
Line (
(<*pf*> @),3)
by A5, MATRIX_0:52
.=
<*(pf . 3)*>
by A1, Th62
;
verum end;
hence
<*pf*> @ = <*<*(pf . 1)*>,<*(pf . 2)*>,<*(pf . 3)*>*>
by FINSEQ_1:45; verum