let K be Field; :: thesis: for pK being FinSequence of
for a being Element of holds len pK = len (a * pK)
let pK be FinSequence of ; :: thesis: for a being Element of holds len pK = len (a * pK)
let a be Element of ; :: 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