let Al be QC-alphabet ; :: thesis: for p being Element of CQC-WFF Al
for f, g being FinSequence of CQC-WFF Al st 0 < len f & |- f ^ <*p*> holds
|- (((Ant f) ^ g) ^ <*(Suc f)*>) ^ <*p*>
let p be Element of CQC-WFF Al; :: thesis: for f, g being FinSequence of CQC-WFF Al st 0 < len f & |- f ^ <*p*> holds
|- (((Ant f) ^ g) ^ <*(Suc f)*>) ^ <*p*>
let f, g be FinSequence of CQC-WFF Al; :: thesis: ( 0 < len f & |- f ^ <*p*> implies |- (((Ant f) ^ g) ^ <*(Suc f)*>) ^ <*p*> )
assume that
A1: 0 < len f and
A2: |- f ^ <*p*> ; :: thesis: |- (((Ant f) ^ g) ^ <*(Suc f)*>) ^ <*p*>
f is_Subsequence_of ((Ant f) ^ g) ^ <*(Suc f)*> by A1, CALCUL_1:13;
then Ant (f ^ <*p*>) is_Subsequence_of ((Ant f) ^ g) ^ <*(Suc f)*> by CALCUL_1:5;
then A3: Ant (f ^ <*p*>) is_Subsequence_of Ant ((((Ant f) ^ g) ^ <*(Suc f)*>) ^ <*p*>) by CALCUL_1:5;
Suc (f ^ <*p*>) = p by CALCUL_1:5;
then Suc (f ^ <*p*>) = Suc ((((Ant f) ^ g) ^ <*(Suc f)*>) ^ <*p*>) by CALCUL_1:5;
hence |- (((Ant f) ^ g) ^ <*(Suc f)*>) ^ <*p*> by A2, A3, CALCUL_1:36; :: thesis: verum