let D be non empty set ; :: thesis: for pf being FinSequence of D st len pf = 3 holds
<*pf*> @ = <*<*(pf . 1)*>,<*(pf . 2)*>,<*(pf . 3)*>*>
let pf be FinSequence of D; :: thesis: ( len pf = 3 implies <*pf*> @ = <*<*(pf . 1)*>,<*(pf . 2)*>,<*(pf . 3)*>*> )
assume A1: len pf = 3 ; :: thesis: <*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 :: thesis: ( 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; :: thesis: ( (<*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 ;
:: thesis: ( (<*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 ;
:: thesis: (<*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 ;
:: thesis: verum

end;

hence <*pf*> @ = <*<*(pf . 1)*>,<*(pf . 2)*>,<*(pf . 3)*>*> by FINSEQ_1:45; :: thesis: verum