let p be Element of CQC-WFF ; :: thesis: for f being FinSequence of CQC-WFF holds
( Suc (f ^ <*p*>) = p & Ant (f ^ <*p*>) = f )
let f be FinSequence of CQC-WFF ; :: thesis: ( Suc (f ^ <*p*>) = p & Ant (f ^ <*p*>) = f )
set fin = f ^ <*p*>;
A1: len (f ^ <*p*>) = (len f) + 1 by FINSEQ_2:19;
thus Suc (f ^ <*p*>) = p :: thesis: Ant (f ^ <*p*>) = f

proof

(f ^ <*p*>) . (len (f ^ <*p*>)) = p by A1, FINSEQ_1:59;
hence Suc (f ^ <*p*>) = p by Def2; :: thesis: verum

end;

thus Ant (f ^ <*p*>) = f :: thesis: verum

proof

set fin = f ^ <*p*>;

now

let a be set ; :: thesis: ( a in f implies a in f ^ <*p*> )
assume a in f ; :: thesis: a in f ^ <*p*>
then consider k being Nat such that
A2: ( k in dom f & a = [k,(f . k)] ) by FINSEQ_1:16;
A3: k in dom (f ^ <*p*>) by A2, FINSEQ_2:18;
f . k = (f ^ <*p*>) . k by A2, FINSEQ_1:def 7;
hence a in f ^ <*p*> by A2, A3, FUNCT_1:8; :: thesis: verum

end;

then f c= f ^ <*p*> by TARSKI:def 3;
then f = (f ^ <*p*>) | (dom f) by GRFUNC_1:64;
then f = (f ^ <*p*>) | (Seg (len f)) by FINSEQ_1:def 3;
hence Ant (f ^ <*p*>) = f by A1, Def1; :: thesis: verum

end;