let D be non empty set ; :: thesis: for S being FinSequence_of_Square-Matrix of D holds Len S = Width S
let S be FinSequence_of_Square-Matrix of D; :: thesis: Len S = Width S
set L = Len S;
set W = Width S;
A1: dom (Width S) = dom S by Def4;
A2: dom (Len S) = dom S by Def3;

now :: thesis: for k being Nat st k in dom (Len S) holds
(Len S) . k = (Width S) . k

let k be Nat; :: thesis: ( k in dom (Len S) implies (Len S) . k = (Width S) . k )
assume A3: k in dom (Len S) ; :: thesis: (Len S) . k = (Width S) . k
thus (Len S) . k = len (S . k) by A3, Def3
.= width (S . k) by MATRIX_0:24
.= (Width S) . k by A2, A1, A3, Def4 ; :: thesis: verum

end;

hence Len S = Width S by A2, A1, FINSEQ_1:13; :: thesis: verum