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 (Len S) = dom S & dom (Width S) = dom S ) by Def3, Def4;

now

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

end;

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