let D be non empty set ; 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; ( Sum (Len F) = 0 implies Sum (Width F) = 0 )
set LF = Len F;
set WF = Width F;
assume A1:
Sum (Len F) = 0
; 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 A2:
for
i being
Nat st
i in dom (Len F) holds
0 >= (Len F) . i
;
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 for j being Nat st 1 <= j & j <= len (Width F) holds
(Width F) . j = ((len F) |-> 0) . jlet j be
Nat;
( 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)
;
(Width F) . j = ((len F) |-> 0) . jA9:
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;
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;
verum end;