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 :: thesis: for i being Nat st i in dom (Len (1. (K,f))) holds
(Len (1. (K,f))) . i = f . i
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_0:24 ; :: thesis: verum
end;
hence Len (1. (K,f)) = f by A2, A1, FINSEQ_1:13; :: thesis: Width (1. (K,f)) = f
A4: dom (Width (1. (K,f))) = dom (1. (K,f)) by Def4;
now :: thesis: for i being Nat st i in dom (Width (1. (K,f))) holds
(Width (1. (K,f))) . i = f . i
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_0:24 ; :: thesis: verum
end;
hence Width (1. (K,f)) = f by A4, A1, FINSEQ_1:13; :: thesis: verum