let K be Field; :: thesis: for G1, G2 being FinSequence_of_Matrix of K st Width G1 = Len G2 holds
( Len (G1 (#) G2) = Len G1 & Width (G1 (#) G2) = Width G2 )
let G1, G2 be FinSequence_of_Matrix of K; :: thesis: ( Width G1 = Len G2 implies ( Len (G1 (#) G2) = Len G1 & Width (G1 (#) G2) = Width G2 ) )
assume A1: Width G1 = Len G2 ; :: thesis: ( Len (G1 (#) G2) = Len G1 & Width (G1 (#) G2) = Width G2 )
set G12 = G1 (#) G2;
A2: ( dom (Len G1) = dom G1 & dom (Len (G1 (#) G2)) = dom (G1 (#) G2) & dom (Width G1) = dom G1 & dom (Len G2) = dom G2 & dom (Width (G1 (#) G2)) = dom (G1 (#) G2) & dom (Width G2) = dom G2 & dom (G1 (#) G2) = dom G1 ) by Def11, Def3, Def4;

now

let i be Nat; :: thesis: ( i in dom (Len (G1 (#) G2)) implies (Len (G1 (#) G2)) . i = (Len G1) . i )
assume A3: i in dom (Len (G1 (#) G2)) ; :: thesis: (Len (G1 (#) G2)) . i = (Len G1) . i
A4: width (G1 . i) = (Width G1) . i by A2, A3, Def4
.= len (G2 . i) by A1, A2, A3, Def3 ;
thus (Len (G1 (#) G2)) . i = len ((G1 (#) G2) . i) by A3, Def3
.= len ((G1 . i) * (G2 . i)) by A2, A3, Def11
.= len (G1 . i) by A4, MATRIX_3:def 4
.= (Len G1) . i by A2, A3, Def3 ; :: thesis: verum

end;

hence Len (G1 (#) G2) = Len G1 by A2, FINSEQ_1:17; :: thesis: Width (G1 (#) G2) = Width G2

now

let i be Nat; :: thesis: ( i in dom (Width (G1 (#) G2)) implies (Width (G1 (#) G2)) . i = (Width G2) . i )
assume A5: i in dom (Width (G1 (#) G2)) ; :: thesis: (Width (G1 (#) G2)) . i = (Width G2) . i
A6: width (G1 . i) = (Width G1) . i by A2, A5, Def4
.= len (G2 . i) by A1, A2, A5, Def3 ;
thus (Width (G1 (#) G2)) . i = width ((G1 (#) G2) . i) by A5, Def4
.= width ((G1 . i) * (G2 . i)) by A2, A5, Def11
.= width (G2 . i) by A6, MATRIX_3:def 4
.= (Width G2) . i by A1, A2, A5, Def4 ; :: thesis: verum

end;

hence Width (G1 (#) G2) = Width G2 by A1, A2, FINSEQ_1:17; :: thesis: verum