let K be non empty multMagma ; :: thesis: for p being FinSequence of K
for a being Element of K holds len (a * p) = len p
let p be FinSequence of K; :: thesis: for a being Element of K holds len (a * p) = len p
let a be Element of K; :: thesis: len (a * p) = len p
reconsider q = p as Element of (len p) -tuples_on the carrier of K by FINSEQ_2:92;
a * q in (len p) -tuples_on the carrier of K ;
then a * q in { s where s is Element of the carrier of K * : len s = len p } by FINSEQ_2:def 4;
then ex s being Element of the carrier of K * st
( a * q = s & len s = len p ) ;
hence len (a * p) = len p ; :: thesis: verum