let D be non empty set ; :: thesis: for F being FinSequence_of_Matrix of D st Sum (Len F) = 0 holds
Sum (Width F) = 0
let F be FinSequence_of_Matrix of D; :: thesis: ( Sum (Len F) = 0 implies Sum (Width F) = 0 )
set LF = Len F;
set WF = Width F;
assume A1: Sum (Len F) = 0 ; :: thesis: Sum (Width F) = 0

per cases ( ex i being Nat st
( i in dom (Len F) & 0 > (Len F) . i ) or for i being Nat st i in dom (Len F) holds
0 >= (Len F) . i ) by A1, RVSUM_1:85;

suppose ex i being Nat st
( i in dom (Len F) & 0 > (Len F) . i ) ; :: thesis: Sum (Width F) = 0

hence Sum (Width F) = 0 ; :: thesis: verum

end;

suppose A2: for i being Nat st i in dom (Len F) holds
0 >= (Len F) . i ; :: thesis: Sum (Width F) = 0

set F0 = (len F) |-> 0;
A3: len (Width F) = len F by CARD_1:def 7;
A4: dom (Len F) = dom F by Def3;
A5: dom (Width F) = dom F by Def4;

A6: now :: thesis: for j being Nat st 1 <= j & j <= len (Width F) holds
(Width F) . j = ((len F) |-> 0) . j

let j be Nat; :: thesis: ( 1 <= j & j <= len (Width F) implies (Width F) . j = ((len F) |-> 0) . j )
assume that
A7: 1 <= j and
A8: j <= len (Width F) ; :: thesis: (Width F) . j = ((len F) |-> 0) . j
A9: j in dom (Width F) by A7, A8, FINSEQ_3:25;
then A10: (Width F) . j = width (F . j) by Def4;
j in Seg (len F) by A3, A7, A8;
then A11: ((len F) |-> 0) . j = 0 by FINSEQ_2:57;
A12: 0 >= (Len F) . j by A2, A5, A4, A9;
(Len F) . j = len (F . j) by A5, A4, A9, Def3;
hence (Width F) . j = ((len F) |-> 0) . j by A10, A12, A11, MATRIX_0:def 3; :: thesis: verum

end;

len ((len F) |-> 0) = len F by CARD_1:def 7;
then Width F = (len F) |-> 0 by A3, A6;
hence Sum (Width F) = 0 by RVSUM_1:81; :: thesis: verum

end;

end;