let p be set ; :: thesis: for f being FinSequence holds Rev (<*p*> ^ f) = (Rev f) ^ <*p*>
let f be FinSequence; :: thesis: Rev (<*p*> ^ f) = (Rev f) ^ <*p*>
thus Rev (<*p*> ^ f) = (Rev f) ^ (Rev <*p*>) by FINSEQ_5:64
.= (Rev f) ^ <*p*> by FINSEQ_5:60 ; :: thesis: verum