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:43;

Rev h = <*z,y*> by FINSEQ_5:61;

hence Rev f = <*z,y,x*> by A1, FINSEQ_6:24; :: thesis: verum

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:43;

Rev h = <*z,y*> by FINSEQ_5:61;

hence Rev f = <*z,y,x*> by A1, FINSEQ_6:24; :: thesis: verum