let n, m be Nat; :: thesis: for F being Function of (Seg n),(Seg n)
for D being non empty set
for M being Matrix of n,m,D
for i being Nat st i in Seg (width M) holds
Col ((M * F),i) = (Col (M,i)) * F
let F be Function of (Seg n),(Seg n); :: thesis: for D being non empty set
for M being Matrix of n,m,D
for i being Nat st i in Seg (width M) holds
Col ((M * F),i) = (Col (M,i)) * F
let D be non empty set ; :: thesis: for M being Matrix of n,m,D
for i being Nat st i in Seg (width M) holds
Col ((M * F),i) = (Col (M,i)) * F
let M be Matrix of n,m,D; :: thesis: for i being Nat st i in Seg (width M) holds
Col ((M * F),i) = (Col (M,i)) * F
let i be Nat; :: thesis: ( i in Seg (width M) implies Col ((M * F),i) = (Col (M,i)) * F )
assume A1: i in Seg (width M) ; :: thesis: Col ((M * F),i) = (Col (M,i)) * F
A2: len M = n by MATRIX_0:def 2;
then A3: dom M = Seg n by FINSEQ_1:def 3;
len (Col (M,i)) = n by A2, CARD_1:def 7;
then A4: dom (Col (M,i)) = Seg n by FINSEQ_1:def 3;
( dom F = Seg n & rng F c= Seg n ) by FUNCT_2:52, RELAT_1:def 19;
then A5: dom ((Col (M,i)) * F) = Seg n by A4, RELAT_1:27;
A6: len (M * F) = n by MATRIX_0:def 2;
then A7: dom (M * F) = Seg n by FINSEQ_1:def 3;

A8: now :: thesis: for x being object st x in Seg n holds
((Col (M,i)) * F) . x = (Col ((M * F),i)) . x

let x be object ; :: thesis: ( x in Seg n implies ((Col (M,i)) * F) . x = (Col ((M * F),i)) . x )
assume A9: x in Seg n ; :: thesis: ((Col (M,i)) * F) . x = (Col ((M * F),i)) . x
then reconsider j = x as Element of NAT ;
Indices M = [:(dom M),(Seg (width M)):] by MATRIX_0:def 4;
then A10: [j,i] in Indices M by A1, A3, A9, ZFMISC_1:87;
A11: F . x in Seg n by A4, A5, A9, FUNCT_1:11;
then reconsider Fj = F . x as Element of NAT ;
thus ((Col (M,i)) * F) . x = (Col (M,i)) . Fj by A5, A9, FUNCT_1:12
.= M * (Fj,i) by A3, A11, MATRIX_0:def 8
.= (M * F) * (j,i) by A10, MATRIX11:def 4
.= (Col ((M * F),i)) . x by A7, A9, MATRIX_0:def 8 ; :: thesis: verum

end;

len (Col ((M * F),i)) = n by A6, CARD_1:def 7;
then dom (Col ((M * F),i)) = Seg n by FINSEQ_1:def 3;
hence Col ((M * F),i) = (Col (M,i)) * F by A5, A8, FUNCT_1:2; :: thesis: verum