let p be FinSequence; :: thesis: ( {} $^ p = p & p $^ {} = p )
( {} ^ p = p & p ^ {} = p ) by FINSEQ_1:34;
hence ( {} $^ p = p & p $^ {} = p ) by Def1; :: thesis: verum