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