let K be Field; for f being FinSequence of NAT holds
( Len (1. (K,f)) = f & Width (1. (K,f)) = f )
let f be FinSequence of NAT ; ( 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 for i being Nat st i in dom (Len (1. (K,f))) holds
(Len (1. (K,f))) . i = f . ilet i be
Nat;
( i in dom (Len (1. (K,f))) implies (Len (1. (K,f))) . i = f . i )assume A3:
i in dom (Len (1. (K,f)))
;
(Len (1. (K,f))) . i = f . ithus (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
;
verum end;
hence
Len (1. (K,f)) = f
by A2, A1, FINSEQ_1:13; Width (1. (K,f)) = f
A4:
dom (Width (1. (K,f))) = dom (1. (K,f))
by Def4;
now for i being Nat st i in dom (Width (1. (K,f))) holds
(Width (1. (K,f))) . i = f . ilet i be
Nat;
( i in dom (Width (1. (K,f))) implies (Width (1. (K,f))) . i = f . i )assume A5:
i in dom (Width (1. (K,f)))
;
(Width (1. (K,f))) . i = f . ithus (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
;
verum end;
hence
Width (1. (K,f)) = f
by A4, A1, FINSEQ_1:13; verum