let f be FinSequence; :: thesis: for x being set holds Rev (f ^ <*x*>) = <*x*> ^ (Rev f)
let x be set ; :: thesis: Rev (f ^ <*x*>) = <*x*> ^ (Rev f)
set n = (len f) + 1;
set g = <*x*>;
A1: len (f ^ <*x*>) = (len f) + 1 by FINSEQ_2:19;
A2: len (<*x*> ^ (Rev f)) = (len <*x*>) + (len (Rev f)) by FINSEQ_1:35
.= 1 + (len (Rev f)) by FINSEQ_1:56
.= (len f) + 1 by Def3 ;
A3: len (Rev (f ^ <*x*>)) = (len f) + 1 by A1, Def3;

now

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

per cases ( i = 1 or i > 1 ) by A5, 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 A6;
thus (Rev (f ^ <*x*>)) . i = (f ^ <*x*>) . ((((len f) + 1) - 1) + 1) by A1, A7, A8, Def3
.= x by FINSEQ_1:59
.= <*x*> . 1 by FINSEQ_1:57
.= (<*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;
reconsider k = (((len f) + 1) - i) + 1 as Element of NAT by A5, Th1;
consider l being Nat such that
A11: i = l + 1 by A10, NAT_1:6;
l <> 0 by A10, A11;
then A12: 1 <= j by A11, NAT_1:14;
j <= ((len f) + 1) - 1 by A5, XREAL_1:11;
then A13: j in dom f by A12, FINSEQ_3:27;
i - i <= ((len f) + 1) - i by A5, XREAL_1:11;
then A14: 0 + 1 <= k by XREAL_1:8;
(len f) + 1 < (len f) + i by A10, XREAL_1:10;
then ((len f) + 1) - i < ((len f) + i) - i by XREAL_1:11;
then k < (len f) + 1 by XREAL_1:8;
then k <= len f by NAT_1:13;
then A15: k in dom f by A14, FINSEQ_3:27;
thus (Rev (f ^ <*x*>)) . i = (f ^ <*x*>) . ((((len f) + 1) - i) + 1) by A1, A7, Def3
.= f . (((len f) - j) + 1) by A15, FINSEQ_1:def 7
.= (Rev f) . j by A13, Th61
.= (<*x*> ^ (Rev f)) . i by A2, A5, A6, A10, FINSEQ_1:37 ; :: thesis: verum

end;

end;

end;

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