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:115;

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

then consider i being Nat such that
A2: ( i in dom (Len F) & 0 > (Len F) . i ) ;
thus Sum (Width F) = 0 by A2; :: thesis: verum

end;

suppose A3: 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 ;
A4: ( len (Width F) = len F & len ((len F) |-> 0 ) = len F ) by FINSEQ_1:def 18, FINSEQ_1:def 18;
A5: ( dom (Width F) = dom F & dom (Len F) = dom F ) by Def3, Def4;

now

let j be Nat; :: thesis: ( 1 <= j & j <= len (Width F) implies (Width F) . j = ((len F) |-> 0 ) . j )
assume A6: ( 1 <= j & j <= len (Width F) ) ; :: thesis: (Width F) . j = ((len F) |-> 0 ) . j
( j in dom (Width F) & len F <> 0 & j in Seg (len F) ) by A4, A6, FINSEQ_1:3, FINSEQ_3:27;
then ( (Width F) . j = width (F . j) & (Len F) . j = len (F . j) & 0 >= (Len F) . j & ((len F) |-> 0 ) . j = 0 ) by A3, A5, Def3, Def4, FINSEQ_2:71;
hence (Width F) . j = ((len F) |-> 0 ) . j by MATRIX_1:def 4; :: thesis: verum

end;

then Width F = (len F) |-> 0 by A4, FINSEQ_1:18;
hence Sum (Width F) = 0 by RVSUM_1:111; :: thesis: verum

end;

end;