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 A0: ( 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 AA1100;
hence |((Base_FinSeq K,m,i),(Base_FinSeq K,m,i))| = (Base_FinSeq K,m,i) . i by A0, AA2627
.= 1. K by AA1110, A0 ;
:: thesis: verum