let D be non empty set ; :: thesis: for pr being FinSequence of D st len pr = 3 holds
( Col (<*pr*>,1) = <*(pr . 1)*> & Col (<*pr*>,2) = <*(pr . 2)*> & Col (<*pr*>,3) = <*(pr . 3)*> )
let pr be FinSequence of D; :: thesis: ( len pr = 3 implies ( Col (<*pr*>,1) = <*(pr . 1)*> & Col (<*pr*>,2) = <*(pr . 2)*> & Col (<*pr*>,3) = <*(pr . 3)*> ) )
assume len pr = 3 ; :: thesis: ( Col (<*pr*>,1) = <*(pr . 1)*> & Col (<*pr*>,2) = <*(pr . 2)*> & Col (<*pr*>,3) = <*(pr . 3)*> )
then A2: Indices <*pr*> = [:(Seg 1),(Seg 3):] by MATRIX_0:23;
consider p being FinSequence of D such that
A3: p = <*pr*> . 1 and
A4: <*pr*> * (1,1) = p . 1 by A2, Th3, MATRIX_0:def 5;
A5: len (Col (<*pr*>,1)) = len <*pr*> by MATRIX_0:def 8;
A6: len <*pr*> = 1 by FINSEQ_1:39;
then A7: dom <*pr*> = Seg 1 by FINSEQ_1:def 3;
then (Col (<*pr*>,1)) . 1 = <*pr*> * (1,1) by FINSEQ_1:1, MATRIX_0:def 8
.= pr . 1 by A4, A3 ;
hence Col (<*pr*>,1) = <*(pr . 1)*> by A6, A5, FINSEQ_1:40; :: thesis: ( Col (<*pr*>,2) = <*(pr . 2)*> & Col (<*pr*>,3) = <*(pr . 3)*> )
consider p being FinSequence of D such that
A8: p = <*pr*> . 1 and
A9: <*pr*> * (1,2) = p . 2 by A2, Th3, MATRIX_0:def 5;
A10: len (Col (<*pr*>,2)) = len <*pr*> by MATRIX_0:def 8;
(Col (<*pr*>,2)) . 1 = <*pr*> * (1,2) by A7, FINSEQ_1:1, MATRIX_0:def 8
.= pr . 2 by A9, A8 ;
hence Col (<*pr*>,2) = <*(pr . 2)*> by A6, A10, FINSEQ_1:40; :: thesis: Col (<*pr*>,3) = <*(pr . 3)*>
consider p being FinSequence of D such that
A11: p = <*pr*> . 1 and
A12: <*pr*> * (1,3) = p . 3 by A2, Th3, MATRIX_0:def 5;
A13: len (Col (<*pr*>,3)) = len <*pr*> by MATRIX_0:def 8;
(Col (<*pr*>,3)) . 1 = <*pr*> * (1,3) by A7, FINSEQ_1:1, MATRIX_0:def 8
.= pr . 3 by A12, A11 ;
hence Col (<*pr*>,3) = <*(pr . 3)*> by A6, A13, FINSEQ_1:40; :: thesis: verum