let x be set ; :: thesis: for f being FinSequence holds
( len (f ^ <*x*>) = (len f) + 1 & len (<*x*> ^ f) = (len f) + 1 & (f ^ <*x*>) . ((len f) + 1) = x & (<*x*> ^ f) . 1 = x )
let f be FinSequence; :: thesis: ( len (f ^ <*x*>) = (len f) + 1 & len (<*x*> ^ f) = (len f) + 1 & (f ^ <*x*>) . ((len f) + 1) = x & (<*x*> ^ f) . 1 = x )
A1: len (<*x*> ^ f) = (len <*x*>) + (len f) by FINSEQ_1:22
.= (len f) + 1 by FINSEQ_1:39 ;
1 <= len <*x*> by FINSEQ_1:39;
then A2: 1 in dom <*x*> by FINSEQ_3:25;
then A3: (<*x*> ^ f) . 1 = <*x*> . 1 by FINSEQ_1:def 7
.= x ;
(f ^ <*x*>) . ((len f) + 1) = <*x*> . 1 by A2, FINSEQ_1:def 7
.= x ;
hence ( len (f ^ <*x*>) = (len f) + 1 & len (<*x*> ^ f) = (len f) + 1 & (f ^ <*x*>) . ((len f) + 1) = x & (<*x*> ^ f) . 1 = x ) by A1, A3, FINSEQ_2:16; :: thesis: verum