let D be non empty set ; :: thesis: for x, y, z being Element of D
for f being FinSequence of D st f = <*x,y,z*> holds
Rev f = <*z,y,x*>
let x, y, z be Element of D; :: thesis: for f being FinSequence of D st f = <*x,y,z*> holds
Rev f = <*z,y,x*>
let f be FinSequence of D; :: thesis: ( f = <*x,y,z*> implies Rev f = <*z,y,x*> )
reconsider h = <*y,z*> as FinSequence of D ;
assume f = <*x,y,z*> ; :: thesis: Rev f = <*z,y,x*>
then A1: f = <*x*> ^ h by FINSEQ_1:60;
Rev h = <*z,y*> by FINSEQ_5:64;
hence Rev f = <*z,y,x*> by A1, FINSEQ_6:28; :: thesis: verum