let n, m be Nat; 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); 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 ; 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; for i being Nat st i in Seg (width M) holds
Col ((M * F),i) = (Col (M,i)) * F
let i be Nat; ( i in Seg (width M) implies Col ((M * F),i) = (Col (M,i)) * F )
assume A1:
i in Seg (width M)
; 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 for x being object st x in Seg n holds
((Col (M,i)) * F) . x = (Col ((M * F),i)) . xlet x be
object ;
( x in Seg n implies ((Col (M,i)) * F) . x = (Col ((M * F),i)) . x )assume A9:
x in Seg n
;
((Col (M,i)) * F) . x = (Col ((M * F),i)) . xthen 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
;
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; verum