let K be Field; :: thesis: for G being FinSequence_of_Matrix of K
for p being FinSequence of K holds
( Len (mlt p,G) = Len G & Width (mlt p,G) = Width G )
let G be FinSequence_of_Matrix of K; :: thesis: for p being FinSequence of K holds
( Len (mlt p,G) = Len G & Width (mlt p,G) = Width G )
let p be FinSequence of K; :: thesis: ( Len (mlt p,G) = Len G & Width (mlt p,G) = Width G )
set M = mlt p,G;
A1: ( dom (Len (mlt p,G)) = dom (mlt p,G) & dom (Len G) = dom G & dom (Width G) = dom G & dom (Width (mlt p,G)) = dom (mlt p,G) & dom (mlt p,G) = dom G ) by Def3, Def4, Def9;

now

let i be Nat; :: thesis: ( i in dom (Len (mlt p,G)) implies (Len (mlt p,G)) . i = (Len G) . i )
assume A2: i in dom (Len (mlt p,G)) ; :: thesis: (Len (mlt p,G)) . i = (Len G) . i
thus (Len (mlt p,G)) . i = len ((mlt p,G) . i) by A2, Def3
.= len ((p /. i) * (G . i)) by A1, A2, Def9
.= len (G . i) by MATRIX_3:def 5
.= (Len G) . i by A1, A2, Def3 ; :: thesis: verum

end;

hence Len (mlt p,G) = Len G by A1, FINSEQ_1:17; :: thesis: Width (mlt p,G) = Width G

now

let i be Nat; :: thesis: ( i in dom (Width (mlt p,G)) implies (Width (mlt p,G)) . i = (Width G) . i )
assume A3: i in dom (Width (mlt p,G)) ; :: thesis: (Width (mlt p,G)) . i = (Width G) . i
thus (Width (mlt p,G)) . i = width ((mlt p,G) . i) by A3, Def4
.= width ((p /. i) * (G . i)) by A1, A3, Def9
.= width (G . i) by MATRIX_3:def 5
.= (Width G) . i by A1, A3, Def4 ; :: thesis: verum

end;

hence Width (mlt p,G) = Width G by A1, FINSEQ_1:17; :: thesis: verum