let a be Complex; for f, g being complex-valued FinSequence st g = Rev f holds
Rev (a (#) f) = a (#) g
let f, g be complex-valued FinSequence; ( g = Rev f implies Rev (a (#) f) = a (#) g )
assume A1:
g = Rev f
; Rev (a (#) f) = a (#) g
set h = a (#) f;
set h1 = a (#) g;
set h2 = Rev (a (#) f);
A2:
( dom (a (#) g) = dom g & dom (a (#) f) = dom f )
by VALUED_1:def 5;
A4:
( dom (Rev (a (#) f)) = dom (a (#) f) & dom (Rev f) = dom f )
by FINSEQ_5:57;
then A5:
( len (a (#) g) = len (Rev (a (#) f)) & len (Rev (a (#) f)) = len f & len f = len (a (#) f) & len g = len f )
by A1, A2, FINSEQ_3:29;
reconsider h1 = a (#) g as len f -element complex-valued FinSequence by A5;
for x being object st x in dom h1 holds
h1 . x = (Rev (a (#) f)) . x
proof
let x be
object ;
( x in dom h1 implies h1 . x = (Rev (a (#) f)) . x )
assume B1:
x in dom h1
;
h1 . x = (Rev (a (#) f)) . x
reconsider x =
x as
Nat by B1;
B3:
( 1
<= x &
x <= len f )
by B1, A1, A2, A4, FINSEQ_3:25;
then reconsider k =
(len f) - x as
Element of
NAT by NAT_1:21;
set l =
k + 1;
B4:
(
0 + 1
<= k + 1 &
k + 1
<= k + x )
by B3, XREAL_1:6;
(Rev (a (#) f)) . x =
(a (#) f) . (((len (a (#) f)) - x) + 1)
by B1, A1, A2, A4, FINSEQ_5:def 3
.=
(a (#) f) . (k + 1)
by A2, FINSEQ_3:29
.=
a * ((Rev (Rev f)) . (k + 1))
by A2, B4, FINSEQ_3:25, VALUED_1:def 5
.=
a * (g . (((len g) - (k + 1)) + 1))
by A1, A4, B4, FINSEQ_3:25, FINSEQ_5:def 3
.=
a * (g . x)
by A5
;
hence
h1 . x = (Rev (a (#) f)) . x
by B1, VALUED_1:def 5;
verum
end;
hence
Rev (a (#) f) = a (#) g
by A1, A2, A4, FUNCT_1:2; verum