let K be Field; for m, i being Element of NAT st 1 <= i & i <= m holds
|((Base_FinSeq (K,m,i)),(Base_FinSeq (K,m,i)))| = 1. K
let m, i be Element of NAT ; ( 1 <= i & i <= m implies |((Base_FinSeq (K,m,i)),(Base_FinSeq (K,m,i)))| = 1. K )
assume A1:
( 1 <= i & i <= m )
; |((Base_FinSeq (K,m,i)),(Base_FinSeq (K,m,i)))| = 1. K
len (Base_FinSeq (K,m,i)) = m
by Th23;
hence |((Base_FinSeq (K,m,i)),(Base_FinSeq (K,m,i)))| =
(Base_FinSeq (K,m,i)) . i
by A1, Th35
.=
1. K
by A1, Th24
;
verum