let k be Nat; :: thesis: for D being non empty set
for pf being FinSequence of D st k in dom pf holds
Col (<*pf*>,k) = <*(pf . k)*>
let D be non empty set ; :: thesis: for pf being FinSequence of D st k in dom pf holds
Col (<*pf*>,k) = <*(pf . k)*>
let pf be FinSequence of D; :: thesis: ( k in dom pf implies Col (<*pf*>,k) = <*(pf . k)*> )
assume A1: k in dom pf ; :: thesis: Col (<*pf*>,k) = <*(pf . k)*>
A2: ( len (Col (<*pf*>,k)) = len <*pf*> & ( for j being Nat st j in dom <*pf*> holds
(Col (<*pf*>,k)) . j = <*pf*> * (j,k) ) ) by MATRIX_0:def 8;
then A3: len (Col (<*pf*>,k)) = 1 by FINSEQ_1:39;
then A4: dom (Col (<*pf*>,k)) = {1} by FINSEQ_1:def 3, FINSEQ_1:2;
(Col (<*pf*>,k)) . 1 = <*pf*> * (1,k) by FINSEQ_5:6, A2;
then rng (Col (<*pf*>,k)) = {(<*pf*> * (1,k))} by A4, FUNCT_1:4;
then rng (Col (<*pf*>,k)) = {(pf . k)} by A1, Th58;
hence Col (<*pf*>,k) = <*(pf . k)*> by A3, FINSEQ_1:39; :: thesis: verum