let A be set ; :: thesis: for D9 being non empty set
for q being FinSequence
for p being FinSequence of A
for f being Function of A,D9 st q = f * p holds
len q = len p
let D9 be non empty set ; :: thesis: for q being FinSequence
for p being FinSequence of A
for f being Function of A,D9 st q = f * p holds
len q = len p
let q be FinSequence; :: thesis: for p being FinSequence of A
for f being Function of A,D9 st q = f * p holds
len q = len p
let p be FinSequence of A; :: thesis: for f being Function of A,D9 st q = f * p holds
len q = len p
let f be Function of A,D9; :: thesis: ( q = f * p implies len q = len p )
( dom f = A & rng p c= A ) by FINSEQ_1:def 4, FUNCT_2:def 1;
hence ( q = f * p implies len q = len p ) by Th27; :: thesis: verum