let g, f be FinSequence; :: thesis: ( len g = len f & ( for i being Nat st i in dom g holds
g . i = f . (((len f) - i) + 1) ) implies ( len f = len g & ( for i being Nat st i in dom f holds
f . i = g . (((len g) - i) + 1) ) ) )
assume that
A9: len g = len f and
A10: for i being Nat st i in dom g holds
g . i = f . (((len f) - i) + 1) ; :: thesis: ( len f = len g & ( for i being Nat st i in dom f holds
f . i = g . (((len g) - i) + 1) ) )
thus len f = len g by A9; :: thesis: for i being Nat st i in dom f holds
f . i = g . (((len g) - i) + 1)
let i be Nat; :: thesis: ( i in dom f implies f . i = g . (((len g) - i) + 1) )
assume A11: i in dom f ; :: thesis: f . i = g . (((len g) - i) + 1)
then i in dom g by A9, FINSEQ_3:29;
then i <= len g by FINSEQ_3:25;
then reconsider j = (len g) - i as Element of NAT by INT_1:5;
i >= 1 by A11, FINSEQ_3:25;
then j + i >= j + 1 by XREAL_1:6;
then j < len g by NAT_1:13;
then ( 1 <= j + 1 & j + 1 <= len g ) by NAT_1:11, NAT_1:13;
then A12: j + 1 in dom g by FINSEQ_3:25;
thus f . i = f . (((len f) - (j + 1)) + 1) by A9
.= g . (((len g) - i) + 1) by A10, A12 ; :: thesis: verum