let Al be QC-alphabet ; :: thesis: for p being Element of CQC-WFF Al
for f being FinSequence of CQC-WFF Al holds |- (f ^ <*p*>) ^ <*p*>
let p be Element of CQC-WFF Al; :: thesis: for f being FinSequence of CQC-WFF Al holds |- (f ^ <*p*>) ^ <*p*>
let f be FinSequence of CQC-WFF Al; :: thesis: |- (f ^ <*p*>) ^ <*p*>
len (f ^ <*p*>) in dom (f ^ <*p*>) by CALCUL_1:10;
then (len f) + (len <*p*>) in dom (f ^ <*p*>) by FINSEQ_1:22;
then A1: (len f) + 1 in dom (f ^ <*p*>) by FINSEQ_1:39;
(f ^ <*p*>) . ((len f) + 1) = p by FINSEQ_1:42;
then p is_tail_of f ^ <*p*> by A1, CALCUL_1:def 16;
then Suc ((f ^ <*p*>) ^ <*p*>) is_tail_of f ^ <*p*> by CALCUL_1:5;
then Suc ((f ^ <*p*>) ^ <*p*>) is_tail_of Ant ((f ^ <*p*>) ^ <*p*>) by CALCUL_1:5;
hence |- (f ^ <*p*>) ^ <*p*> by CALCUL_1:33; :: thesis: verum