let K be Ring; :: 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:92;
then a * pK is Element of (len pK) -tuples_on the carrier of K by FINSEQ_2:113;
hence len pK = len (a * pK) by CARD_1:def 7; :: thesis: verum