let f be FinSequence; :: thesis: for x being object holds Rev (f ^ <*x*>) = <*x*> ^ (Rev f)
let x be object ; :: thesis: Rev (f ^ <*x*>) = <*x*> ^ (Rev f)
set n = (len f) + 1;
set g = <*x*>;
A1: len (<*x*> ^ (Rev f)) = (len <*x*>) + (len (Rev f)) by FINSEQ_1:22
.= 1 + (len (Rev f)) by FINSEQ_1:39
.= (len f) + 1 by Def3 ;
A2: len (f ^ <*x*>) = (len f) + 1 by FINSEQ_2:16;
then A3: len (Rev (f ^ <*x*>)) = (len f) + 1 by Def3;

now :: thesis: for i being Nat st i in dom (Rev (f ^ <*x*>)) holds
(Rev (f ^ <*x*>)) . i = (<*x*> ^ (Rev f)) . i

let i be Nat; :: thesis: ( i in dom (Rev (f ^ <*x*>)) implies (Rev (f ^ <*x*>)) . b₁ = (<*x*> ^ (Rev f)) . b₁ )
A4: len <*x*> = 1 by FINSEQ_1:40;
assume A5: i in dom (Rev (f ^ <*x*>)) ; :: thesis: (Rev (f ^ <*x*>)) . b₁ = (<*x*> ^ (Rev f)) . b₁
then A6: 1 <= i by FINSEQ_3:25;
A7: i <= (len f) + 1 by A3, A5, FINSEQ_3:25;

per cases ( i = 1 or i > 1 ) by A6, XXREAL_0:1;

suppose A8: i = 1 ; :: thesis: (Rev (f ^ <*x*>)) . b₁ = (<*x*> ^ (Rev f)) . b₁

Seg (len <*x*>) = dom <*x*> by FINSEQ_1:def 3;
then A9: 1 in dom <*x*> by A4;
thus (Rev (f ^ <*x*>)) . i = (f ^ <*x*>) . ((((len f) + 1) - 1) + 1) by A2, A5, A8, Def3
.= <*x*> . 1 by FINSEQ_1:42
.= (<*x*> ^ (Rev f)) . i by A8, A9, FINSEQ_1:def 7 ; :: thesis: verum

end;

suppose A10: i > 1 ; :: thesis: (Rev (f ^ <*x*>)) . b₁ = (<*x*> ^ (Rev f)) . b₁

then reconsider j = i - 1 as Element of NAT by NAT_1:20;
consider l being Nat such that
A11: i = l + 1 by A10, NAT_1:6;
reconsider k = (((len f) + 1) - i) + 1 as Element of NAT by A7, Th1;
(len f) + 1 < (len f) + i by A10, XREAL_1:8;
then ((len f) + 1) - i < ((len f) + i) - i by XREAL_1:9;
then k < (len f) + 1 by XREAL_1:6;
then A12: k <= len f by NAT_1:13;
i - i <= ((len f) + 1) - i by A7, XREAL_1:9;
then 0 + 1 <= k by XREAL_1:6;
then A13: k in dom f by A12, FINSEQ_3:25;
l <> 0 by A10, A11;
then A14: 1 <= j by A11, NAT_1:14;
j <= ((len f) + 1) - 1 by A7, XREAL_1:9;
then A15: j in dom f by A14, FINSEQ_3:25;
thus (Rev (f ^ <*x*>)) . i = (f ^ <*x*>) . ((((len f) + 1) - i) + 1) by A2, A5, Def3
.= f . (((len f) - j) + 1) by A13, FINSEQ_1:def 7
.= (Rev f) . j by A15, Th58
.= (<*x*> ^ (Rev f)) . i by A1, A7, A4, A10, FINSEQ_1:24 ; :: thesis: verum

end;

end;

end;

hence Rev (f ^ <*x*>) = <*x*> ^ (Rev f) by A1, A3, FINSEQ_2:9; :: thesis: verum