let Al be QC-alphabet ; :: thesis: for p being Element of CQC-WFF Al
for f being FinSequence of CQC-WFF Al holds
( Suc (f ^ <*p*>) = p & Ant (f ^ <*p*>) = f )
let p be Element of CQC-WFF Al; :: thesis: for f being FinSequence of CQC-WFF Al holds
( Suc (f ^ <*p*>) = p & Ant (f ^ <*p*>) = f )
let f be FinSequence of CQC-WFF Al; :: thesis: ( Suc (f ^ <*p*>) = p & Ant (f ^ <*p*>) = f )
set fin = f ^ <*p*>;
A1: len (f ^ <*p*>) = (len f) + 1 by FINSEQ_2:16;
then (f ^ <*p*>) . (len (f ^ <*p*>)) = p by FINSEQ_1:42;
hence Suc (f ^ <*p*>) = p by Def2; :: thesis: Ant (f ^ <*p*>) = f
thus Ant (f ^ <*p*>) = f :: thesis: verum
proof
set fin = f ^ <*p*>;
now :: thesis: for a being object st a in f holds
a in f ^ <*p*>
let a be object ; :: 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 and
A3: a = [k,(f . k)] by FINSEQ_1:12;
( k in dom (f ^ <*p*>) & f . k = (f ^ <*p*>) . k ) by A2, FINSEQ_1:def 7, FINSEQ_2:15;
hence a in f ^ <*p*> by A3, FUNCT_1:1; :: thesis: verum
end;
then f c= f ^ <*p*> ;
then f = (f ^ <*p*>) | (dom f) by GRFUNC_1:23;
then f = (f ^ <*p*>) | (Seg (len f)) by FINSEQ_1:def 3;
hence Ant (f ^ <*p*>) = f by A1, Def1; :: thesis: verum
end;