let K be Field; :: thesis: for G1, G2 being FinSequence_of_Matrix of K holds
( Len (G1 (+) G2) = Len G1 & Width (G1 (+) G2) = Width G1 )
let G1, G2 be FinSequence_of_Matrix of K; :: thesis: ( Len (G1 (+) G2) = Len G1 & Width (G1 (+) G2) = Width G1 )
set G12 = G1 (+) G2;
A1: dom (Len (G1 (+) G2)) = dom (G1 (+) G2) by Def3;
A2: dom (G1 (+) G2) = dom G1 by Def10;
A3: 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 A4: i in dom (Len (G1 (+) G2)) ; :: thesis: (Len (G1 (+) G2)) . i = (Len G1) . i
thus (Len (G1 (+) G2)) . i = len ((G1 (+) G2) . i) by A4, Def3
.= len ((G1 . i) + (G2 . i)) by A1, A4, Def10
.= len (G1 . i) by MATRIX_3:def 3
.= (Len G1) . i by A3, A1, A2, A4, Def3 ; :: thesis: verum

end;

hence Len (G1 (+) G2) = Len G1 by A3, A1, A2, FINSEQ_1:13; :: thesis: Width (G1 (+) G2) = Width G1
A5: dom (Width (G1 (+) G2)) = dom (G1 (+) G2) by Def4;
A6: dom (Width G1) = dom G1 by Def4;

now :: thesis: for i being Nat st i in dom (Width (G1 (+) G2)) holds
(Width (G1 (+) G2)) . i = (Width G1) . i

let i be Nat; :: thesis: ( i in dom (Width (G1 (+) G2)) implies (Width (G1 (+) G2)) . i = (Width G1) . i )
assume A7: i in dom (Width (G1 (+) G2)) ; :: thesis: (Width (G1 (+) G2)) . i = (Width G1) . i
thus (Width (G1 (+) G2)) . i = width ((G1 (+) G2) . i) by A7, Def4
.= width ((G1 . i) + (G2 . i)) by A5, A7, Def10
.= width (G1 . i) by MATRIX_3:def 3
.= (Width G1) . i by A6, A5, A2, A7, Def4 ; :: thesis: verum

end;

hence Width (G1 (+) G2) = Width G1 by A6, A5, A2, FINSEQ_1:13; :: thesis: verum