let K be Field; :: thesis: for pK being FinSequence of K
for a being Element of K holds len pK = len (a * pK)
let pK be FinSequence of K; :: thesis: for a being Element of K holds len pK = len (a * pK)
let a be Element of K; :: thesis: len pK = len (a * pK)
pK is Element of (len pK) -tuples_on the carrier of K by FINSEQ_2:110;
then a * pK is Element of (len pK) -tuples_on the carrier of K by FINSEQ_2:133;
hence len pK = len (a * pK) by FINSEQ_1:def 18; :: thesis: verum