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 (#) G2)) = dom (G1 (#) G2) by Def3;
A3: dom (G1 (#) G2) = dom G1 by Def11;
A4: dom (Width G2) = dom G2 by Def4;
A5: dom (Width G1) = dom G1 by Def4;
A6: dom (Len G1) = dom G1 by Def3;
now :: thesis: for i being Nat st i in dom (Len (G1 (#) G2)) holds
(Len (G1 (#) G2)) . i = (Len G1) . i
let i be Nat; :: thesis: ( i in dom (Len (G1 (#) G2)) implies (Len (G1 (#) G2)) . i = (Len G1) . i )
assume A7: i in dom (Len (G1 (#) G2)) ; :: thesis: (Len (G1 (#) G2)) . i = (Len G1) . i
A8: width (G1 . i) = (Width G1) . i by A2, A5, A3, A7, Def4
.= len (G2 . i) by A1, A2, A5, A3, A7, Def3 ;
thus (Len (G1 (#) G2)) . i = len ((G1 (#) G2) . i) by A7, Def3
.= len ((G1 . i) * (G2 . i)) by A2, A7, Def11
.= len (G1 . i) by A8, MATRIX_3:def 4
.= (Len G1) . i by A6, A2, A3, A7, Def3 ; :: thesis: verum
end;
hence Len (G1 (#) G2) = Len G1 by A6, A2, A3, FINSEQ_1:13; :: thesis: Width (G1 (#) G2) = Width G2
A9: dom (Width (G1 (#) G2)) = dom (G1 (#) G2) by Def4;
A10: dom (Len G2) = dom G2 by Def3;
now :: thesis: for i being Nat st i in dom (Width (G1 (#) G2)) holds
(Width (G1 (#) G2)) . i = (Width G2) . i
let i be Nat; :: thesis: ( i in dom (Width (G1 (#) G2)) implies (Width (G1 (#) G2)) . i = (Width G2) . i )
assume A11: i in dom (Width (G1 (#) G2)) ; :: thesis: (Width (G1 (#) G2)) . i = (Width G2) . i
A12: width (G1 . i) = (Width G1) . i by A5, A9, A3, A11, Def4
.= len (G2 . i) by A1, A5, A9, A3, A11, Def3 ;
thus (Width (G1 (#) G2)) . i = width ((G1 (#) G2) . i) by A11, Def4
.= width ((G1 . i) * (G2 . i)) by A9, A11, Def11
.= width (G2 . i) by A12, MATRIX_3:def 4
.= (Width G2) . i by A1, A5, A10, A9, A4, A3, A11, Def4 ; :: thesis: verum
end;
hence Width (G1 (#) G2) = Width G2 by A1, A5, A10, A9, A4, A3, FINSEQ_1:13; :: thesis: verum