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

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