let D be non empty set ; :: thesis: for pf being FinSequence of D st len pf = 3 holds
( Line ((<*pf*> @),1) = <*(pf . 1)*> & Line ((<*pf*> @),2) = <*(pf . 2)*> & Line ((<*pf*> @),3) = <*(pf . 3)*> )
let pf be FinSequence of D; :: thesis: ( len pf = 3 implies ( Line ((<*pf*> @),1) = <*(pf . 1)*> & Line ((<*pf*> @),2) = <*(pf . 2)*> & Line ((<*pf*> @),3) = <*(pf . 3)*> ) )
assume A1: len pf = 3 ; :: thesis: ( Line ((<*pf*> @),1) = <*(pf . 1)*> & Line ((<*pf*> @),2) = <*(pf . 2)*> & Line ((<*pf*> @),3) = <*(pf . 3)*> )
A3: width <*pf*> = 3 by A1, Th61;
1 in Seg (width <*pf*>) by A3, FINSEQ_1:1;
hence Line ((<*pf*> @),1) = Col (<*pf*>,1) by MATRIX_0:59
.= <*(pf . 1)*> by A1, Th51 ;
:: thesis: ( Line ((<*pf*> @),2) = <*(pf . 2)*> & Line ((<*pf*> @),3) = <*(pf . 3)*> )
2 in Seg (width <*pf*>) by A3, FINSEQ_1:1;
hence Line ((<*pf*> @),2) = Col (<*pf*>,2) by MATRIX_0:59
.= <*(pf . 2)*> by A1, Th51 ;
:: thesis: Line ((<*pf*> @),3) = <*(pf . 3)*>
3 in Seg (width <*pf*>) by A3, FINSEQ_1:1;
hence Line ((<*pf*> @),3) = Col (<*pf*>,3) by MATRIX_0:59
.= <*(pf . 3)*> by A1, Th51 ;
:: thesis: verum