let D be non empty set ; 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; for f being FinSequence of D st f = <*x,y,z*> holds
Rev f = <*z,y,x*>
let f be FinSequence of D; ( f = <*x,y,z*> implies Rev f = <*z,y,x*> )
reconsider h = <*y,z*> as FinSequence of D ;
assume
f = <*x,y,z*>
; 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; verum