let K be Field; :: thesis: 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 ; :: thesis: ( 1 <= i & i <= m implies |((Base_FinSeq (K,m,i)),(Base_FinSeq (K,m,i)))| = 1. K )
assume A1: ( 1 <= i & i <= m ) ; :: thesis: |((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 ;
:: thesis: verum