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