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)) by Def3;
A2: dom (mlt (p,G)) = dom G by Def9;
A3: dom (Len G) = dom G by Def3;

now :: thesis: for i being Nat st i in dom (Len (mlt (p,G))) holds
(Len (mlt (p,G))) . i = (Len G) . i

let i be Nat; :: thesis: ( i in dom (Len (mlt (p,G))) implies (Len (mlt (p,G))) . i = (Len G) . i )
assume A4: 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 A4, Def3
.= len ((p /. i) * (G . i)) by A1, A4, Def9
.= len (G . i) by MATRIX_3:def 5
.= (Len G) . i by A1, A3, A2, A4, Def3 ; :: thesis: verum

end;

hence Len (mlt (p,G)) = Len G by A1, A3, A2, FINSEQ_1:13; :: thesis: Width (mlt (p,G)) = Width G
A5: dom (Width (mlt (p,G))) = dom (mlt (p,G)) by Def4;
A6: dom (Width G) = dom G by Def4;

now :: thesis: for i being Nat st i in dom (Width (mlt (p,G))) holds
(Width (mlt (p,G))) . i = (Width G) . i

let i be Nat; :: thesis: ( i in dom (Width (mlt (p,G))) implies (Width (mlt (p,G))) . i = (Width G) . i )
assume A7: 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 A7, Def4
.= width ((p /. i) * (G . i)) by A5, A7, Def9
.= width (G . i) by MATRIX_3:def 5
.= (Width G) . i by A6, A5, A2, A7, Def4 ; :: thesis: verum

end;

hence Width (mlt (p,G)) = Width G by A6, A5, A2, FINSEQ_1:13; :: thesis: verum