let K be Field; :: thesis: for f being FinSequence of NAT holds
( Len (1. K,f) = f & Width (1. K,f) = f )
let f be FinSequence of NAT ; :: thesis: ( Len (1. K,f) = f & Width (1. K,f) = f )
set ONE = 1. K,f;
A1: dom (1. K,f) = dom f by Def8;
A2: dom (Len (1. K,f)) = dom (1. K,f) by Def3;

now

let i be Nat; :: thesis: ( i in dom (Len (1. K,f)) implies (Len (1. K,f)) . i = f . i )
assume A3: i in dom (Len (1. K,f)) ; :: thesis: (Len (1. K,f)) . i = f . i
thus (Len (1. K,f)) . i = len ((1. K,f) . i) by A3, Def3
.= len (1. K,(f . i)) by A2, A3, Def8
.= f . i by MATRIX_1:25 ; :: thesis: verum

end;

hence Len (1. K,f) = f by A2, A1, FINSEQ_1:17; :: thesis: Width (1. K,f) = f
A4: dom (Width (1. K,f)) = dom (1. K,f) by Def4;

now

let i be Nat; :: thesis: ( i in dom (Width (1. K,f)) implies (Width (1. K,f)) . i = f . i )
assume A5: i in dom (Width (1. K,f)) ; :: thesis: (Width (1. K,f)) . i = f . i
thus (Width (1. K,f)) . i = width ((1. K,f) . i) by A5, Def4
.= width (1. K,(f . i)) by A4, A5, Def8
.= f . i by MATRIX_1:25 ; :: thesis: verum

end;

hence Width (1. K,f) = f by A4, A1, FINSEQ_1:17; :: thesis: verum