let K be non empty multMagma ; :: thesis: for p being FinSequence of
for a being Element of holds len (a * p) = len p
let p be FinSequence of ; :: thesis: for a being Element of holds len (a * p) = len p
let a be Element of ; :: thesis: len (a * p) = len p
reconsider q = p as Element of (len p) -tuples_on the carrier of K by FINSEQ_2:110;
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